Metamath Proof Explorer


Theorem imp45

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

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

Proof

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