Metamath Proof Explorer


Theorem imp43

Description: An importation inference. (Contributed by NM, 26-Apr-1994)

Ref Expression
Hypothesis imp4.1 φ ψ χ θ τ
Assertion imp43 φ ψ χ θ τ

Proof

Step Hyp Ref Expression
1 imp4.1 φ ψ χ θ τ
2 1 imp4b φ ψ χ θ τ
3 2 imp φ ψ χ θ τ