Metamath Proof Explorer


Theorem imp4c

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

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

Proof

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