Theorem oibabs 493

Description: Absorption of disjunction into equivalence.

Assertion

Ref	Expression
oibabs	⊢ ((φ ↔ ψ) ↔ ((φ ∨ ψ) → (φ ↔ ψ)))

Proof of Theorem oibabs

Step	Hyp	Ref	Expression
1		ax-1 3	. 2 ⊢ ((φ ↔ ψ) → ((φ ∨ ψ) → (φ ↔ ψ)))
2		orc 225	. . . . 5 ⊢ (φ → (φ ∨ ψ))
3	2	syl4 19	. . . 4 ⊢ (((φ ∨ ψ) → (φ ↔ ψ)) → (φ → (φ ↔ ψ)))
4	3	ibd 451	. . 3 ⊢ (((φ ∨ ψ) → (φ ↔ ψ)) → (φ → ψ))
5		olc 224	. . . . 5 ⊢ (ψ → (φ ∨ ψ))
6	5	syl4 19	. . . 4 ⊢ (((φ ∨ ψ) → (φ ↔ ψ)) → (ψ → (φ ↔ ψ)))
7		ibib 448	. . . . 5 ⊢ ((ψ → φ) ↔ (ψ → (ψ ↔ φ)))
8		bicom 398	. . . . . 6 ⊢ ((ψ ↔ φ) ↔ (φ ↔ ψ))
9	8	imbi2i 160	. . . . 5 ⊢ ((ψ → (ψ ↔ φ)) ↔ (ψ → (φ ↔ ψ)))
10	7, 9	bitr 151	. . . 4 ⊢ ((ψ → φ) ↔ (ψ → (φ ↔ ψ)))
11	6, 10	sylibr 175	. . 3 ⊢ (((φ ∨ ψ) → (φ ↔ ψ)) → (ψ → φ))
12	4, 11	impbid 397	. 2 ⊢ (((φ ∨ ψ) → (φ ↔ ψ)) → (φ ↔ ψ))
13	1, 12	impbi 139	1 ⊢ ((φ ↔ ψ) ↔ ((φ ∨ ψ) → (φ ↔ ψ)))

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