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

Metamath Proof Explorer

Theorem e33an

Description: Conjunction form of e33 . (Contributed by Alan Sare, 15-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses e33an.1 ⊢ φ , ψ , χ → θ
e33an.2 ⊢ φ , ψ , χ → τ
e33an.3 ⊢ θ ∧ τ → η
Assertion e33an ⊢ φ , ψ , χ → η

Proof

Step Hyp Ref Expression
1 e33an.1 ⊢ φ , ψ , χ → θ
2 e33an.2 ⊢ φ , ψ , χ → τ
3 e33an.3 ⊢ θ ∧ τ → η
4 3 ex ⊢ θ → τ → η
5 1 2 4 e33 ⊢ φ , ψ , χ → η