Metamath Proof Explorer


Theorem imp4d

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

Ref Expression
Hypothesis imp4.1 ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜃𝜏 ) ) ) )
Assertion imp4d ( 𝜑 → ( ( 𝜓 ∧ ( 𝜒𝜃 ) ) → 𝜏 ) )

Proof

Step Hyp Ref Expression
1 imp4.1 ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜃𝜏 ) ) ) )
2 1 imp4a ( 𝜑 → ( 𝜓 → ( ( 𝜒𝜃 ) → 𝜏 ) ) )
3 2 impd ( 𝜑 → ( ( 𝜓 ∧ ( 𝜒𝜃 ) ) → 𝜏 ) )