Theorem pm2.85 439

Description: Theorem *2.85 of [WhiteheadRussell] p. 108.

Assertion

Ref	Expression
pm2.85	⊢ (((φ ∨ ψ) → (φ ∨ χ)) → (φ ∨ (ψ → χ)))

Proof of Theorem pm2.85

Step	Hyp	Ref	Expression
1		imor 204	. . 3 ⊢ (((φ ∨ ψ) → (φ ∨ χ)) ↔ (¬ (φ ∨ ψ) ∨ (φ ∨ χ)))
2		pm2.48 230	. . . 4 ⊢ (¬ (φ ∨ ψ) → (φ ∨ ¬ ψ))
3	2	orim1i 272	. . 3 ⊢ ((¬ (φ ∨ ψ) ∨ (φ ∨ χ)) → ((φ ∨ ¬ ψ) ∨ (φ ∨ χ)))
4	1, 3	sylbi 174	. 2 ⊢ (((φ ∨ ψ) → (φ ∨ χ)) → ((φ ∨ ¬ ψ) ∨ (φ ∨ χ)))
5		imor 204	. . . 4 ⊢ ((ψ → χ) ↔ (¬ ψ ∨ χ))
6	5	orbi2i 214	. . 3 ⊢ ((φ ∨ (ψ → χ)) ↔ (φ ∨ (¬ ψ ∨ χ)))
7		orordi 222	. . 3 ⊢ ((φ ∨ (¬ ψ ∨ χ)) ↔ ((φ ∨ ¬ ψ) ∨ (φ ∨ χ)))
8	6, 7	bitr2 152	. 2 ⊢ (((φ ∨ ¬ ψ) ∨ (φ ∨ χ)) ↔ (φ ∨ (ψ → χ)))
9	4, 8	sylib 173	1 ⊢ (((φ ∨ ψ) → (φ ∨ χ)) → (φ ∨ (ψ → χ)))

Syntax hints:  ¬ wn 1   → wi 2   ∨ wo 195

This theorem is referenced by:  orbidi 510

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