Theorem pm4.78 354

Description: Theorem *4.78 of [WhiteheadRussell] p. 121.

Assertion

Ref	Expression
pm4.78	⊢ (((φ → ψ) ⋁ (φ → χ)) ↔ (φ → (ψ ⋁ χ)))

Proof of Theorem pm4.78

Step	Hyp	Ref	Expression
1		impexp 347	. . 3 ⊢ (((φ ⋀ ¬ ψ) → (φ → χ)) ↔ (φ → (¬ ψ → (φ → χ))))
2		annim 238	. . . 4 ⊢ ((φ ⋀ ¬ ψ) ↔ ¬ (φ → ψ))
3	2	imbi1i 186	. . 3 ⊢ (((φ ⋀ ¬ ψ) → (φ → χ)) ↔ (¬ (φ → ψ) → (φ → χ)))
4		bi2.04 160	. . . . 5 ⊢ ((¬ ψ → (φ → χ)) ↔ (φ → (¬ ψ → χ)))
5	4	imbi2i 185	. . . 4 ⊢ ((φ → (¬ ψ → (φ → χ))) ↔ (φ → (φ → (¬ ψ → χ))))
6		pm5.4 167	. . . 4 ⊢ ((φ → (φ → (¬ ψ → χ))) ↔ (φ → (¬ ψ → χ)))
7	5, 6	bitr 173	. . 3 ⊢ ((φ → (¬ ψ → (φ → χ))) ↔ (φ → (¬ ψ → χ)))
8	1, 3, 7	3bitr3 181	. 2 ⊢ ((¬ (φ → ψ) → (φ → χ)) ↔ (φ → (¬ ψ → χ)))
9		df-or 224	. 2 ⊢ (((φ → ψ) ⋁ (φ → χ)) ↔ (¬ (φ → ψ) → (φ → χ)))
10		df-or 224	. . 3 ⊢ ((ψ ⋁ χ) ↔ (¬ ψ → χ))
11	10	imbi2i 185	. 2 ⊢ ((φ → (ψ ⋁ χ)) ↔ (φ → (¬ ψ → χ)))
12	8, 9, 11	3bitr4 183	1 ⊢ (((φ → ψ) ⋁ (φ → χ)) ↔ (φ → (ψ ⋁ χ)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223

This theorem is referenced by:  pm4.79 355

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

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain