Theorem oibabs 493

Description: Absorption of disjunction into equivalence.

Assertion

Ref	Expression
oibabs	|- ((ph <-> ps) <-> ((ph \/ ps) -> (ph <-> ps)))

Proof of Theorem oibabs

Step	Hyp	Ref	Expression
1		ax-1 3	. 2 |- ((ph <-> ps) -> ((ph \/ ps) -> (ph <-> ps)))
2		orc 225	. . . . 5 |- (ph -> (ph \/ ps))
3	2	syl4 19	. . . 4 |- (((ph \/ ps) -> (ph <-> ps)) -> (ph -> (ph <-> ps)))
4	3	ibd 451	. . 3 |- (((ph \/ ps) -> (ph <-> ps)) -> (ph -> ps))
5		olc 224	. . . . 5 |- (ps -> (ph \/ ps))
6	5	syl4 19	. . . 4 |- (((ph \/ ps) -> (ph <-> ps)) -> (ps -> (ph <-> ps)))
7		ibib 448	. . . . 5 |- ((ps -> ph) <-> (ps -> (ps <-> ph)))
8		bicom 398	. . . . . 6 |- ((ps <-> ph) <-> (ph <-> ps))
9	8	imbi2i 160	. . . . 5 |- ((ps -> (ps <-> ph)) <-> (ps -> (ph <-> ps)))
10	7, 9	bitr 151	. . . 4 |- ((ps -> ph) <-> (ps -> (ph <-> ps)))
11	6, 10	sylibr 175	. . 3 |- (((ph \/ ps) -> (ph <-> ps)) -> (ps -> ph))
12	4, 11	impbid 397	. 2 |- (((ph \/ ps) -> (ph <-> ps)) -> (ph <-> ps))
13	1, 12	impbi 139	1 |- ((ph <-> ps) <-> ((ph \/ ps) -> (ph <-> ps)))

Syntax hints:   -> wi 2   <-> wb 127   \/ wo 195

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org