Metamath Proof Explorer


Theorem imp41

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

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

Proof

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