This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Propositional calculus Logical disjunction pm4.78
Description: Implication distributes over disjunction. Theorem *4.78 of
WhiteheadRussell p. 121. (Contributed by NM , 3-Jan-2005) (Proof
shortened by Wolf Lammen , 19-Nov-2012)
Ref
Expression
Assertion
pm4.78 ⊢ φ → ψ ∨ φ → χ ↔ φ → ψ ∨ χ
Proof
Step
Hyp
Ref
Expression
1
orordi ⊢ ¬ φ ∨ ψ ∨ χ ↔ ¬ φ ∨ ψ ∨ ¬ φ ∨ χ
2
imor ⊢ φ → ψ ∨ χ ↔ ¬ φ ∨ ψ ∨ χ
3
imor ⊢ φ → ψ ↔ ¬ φ ∨ ψ
4
imor ⊢ φ → χ ↔ ¬ φ ∨ χ
5
3 4
orbi12i ⊢ φ → ψ ∨ φ → χ ↔ ¬ φ ∨ ψ ∨ ¬ φ ∨ χ
6
1 2 5
3bitr4ri ⊢ φ → ψ ∨ φ → χ ↔ φ → ψ ∨ χ