Metamath Proof Explorer


Theorem e21an

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

Ref Expression
Hypotheses e21an.1 φ , ψ χ
e21an.2 φ θ
e21an.3 χ θ τ
Assertion e21an φ , ψ τ

Proof

Step Hyp Ref Expression
1 e21an.1 φ , ψ χ
2 e21an.2 φ θ
3 e21an.3 χ θ τ
4 3 ex χ θ τ
5 1 2 4 e21 φ , ψ τ