Metamath Proof Explorer


Theorem imp4b

Description: An importation inference. (Contributed by NM, 26-Apr-1994) Shorten imp4a . (Revised by Wolf Lammen, 19-Jul-2021)

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

Proof

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