Metamath Proof Explorer

Theorem ex-natded9.20-2

Description: A more efficient proof of Theorem 9.20 of Clemente p. 45. Compare with ex-natded9.20 . (Contributed by David A. Wheeler, 19-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ex-natded9.20.1 ⊢ φ → ψ ∧ χ ∨ θ
Assertion ex-natded9.20-2 ⊢ φ → ψ ∧ χ ∨ ψ ∧ θ

Proof

Step Hyp Ref Expression
1 ex-natded9.20.1 ⊢ φ → ψ ∧ χ ∨ θ
2 1 simpld ⊢ φ → ψ
3 2 anim1i ⊢ φ ∧ χ → ψ ∧ χ
4 3 orcd ⊢ φ ∧ χ → ψ ∧ χ ∨ ψ ∧ θ
5 2 anim1i ⊢ φ ∧ θ → ψ ∧ θ
6 5 olcd ⊢ φ ∧ θ → ψ ∧ χ ∨ ψ ∧ θ
7 1 simprd ⊢ φ → χ ∨ θ
8 4 6 7 mpjaodan ⊢ φ → ψ ∧ χ ∨ ψ ∧ θ