This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem im2anan9r

Description: Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996)

Ref Expression
Hypotheses im2an9.1 ⊢ φ → ψ → χ
im2an9.2 ⊢ θ → τ → η
Assertion im2anan9r ⊢ θ ∧ φ → ψ ∧ τ → χ ∧ η

Proof

Step Hyp Ref Expression
1 im2an9.1 ⊢ φ → ψ → χ
2 im2an9.2 ⊢ θ → τ → η
3 1 2 im2anan9 ⊢ φ ∧ θ → ψ ∧ τ → χ ∧ η
4 3 ancoms ⊢ θ ∧ φ → ψ ∧ τ → χ ∧ η