Metamath Proof Explorer


Theorem jad

Description: Deduction form of ja . (Contributed by Scott Fenton, 13-Dec-2010) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Hypotheses jad.1 ( 𝜑 → ( ¬ 𝜓𝜃 ) )
jad.2 ( 𝜑 → ( 𝜒𝜃 ) )
Assertion jad ( 𝜑 → ( ( 𝜓𝜒 ) → 𝜃 ) )

Proof

Step Hyp Ref Expression
1 jad.1 ( 𝜑 → ( ¬ 𝜓𝜃 ) )
2 jad.2 ( 𝜑 → ( 𝜒𝜃 ) )
3 1 com12 ( ¬ 𝜓 → ( 𝜑𝜃 ) )
4 2 com12 ( 𝜒 → ( 𝜑𝜃 ) )
5 3 4 ja ( ( 𝜓𝜒 ) → ( 𝜑𝜃 ) )
6 5 com12 ( 𝜑 → ( ( 𝜓𝜒 ) → 𝜃 ) )