Metamath Proof Explorer


Theorem ex3

Description: Apply ex to a hypothesis with a 3-right-nested conjunction antecedent, with the antecedent of the assertion being a triple conjunction rather than a 2-right-nested conjunction. (Contributed by Alan Sare, 22-Apr-2018)

Ref Expression
Hypothesis ex3.1 φ ψ χ θ τ
Assertion ex3 φ ψ χ θ τ

Proof

Step Hyp Ref Expression
1 ex3.1 φ ψ χ θ τ
2 1 ex φ ψ χ θ τ
3 2 3impa φ ψ χ θ τ