Metamath Proof Explorer


Theorem imp31

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

Ref Expression
Hypothesis imp31.1 φ ψ χ θ
Assertion imp31 φ ψ χ θ

Proof

Step Hyp Ref Expression
1 imp31.1 φ ψ χ θ
2 1 imp φ ψ χ θ
3 2 imp φ ψ χ θ