Metamath Proof Explorer


Theorem exp4d

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

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

Proof

Step Hyp Ref Expression
1 exp4d.1 ( 𝜑 → ( ( 𝜓 ∧ ( 𝜒𝜃 ) ) → 𝜏 ) )
2 1 expd ( 𝜑 → ( 𝜓 → ( ( 𝜒𝜃 ) → 𝜏 ) ) )
3 2 exp4a ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜃𝜏 ) ) ) )