Metamath Proof Explorer


Theorem jaoded

Description: Deduction form of jao . Disjunction of antecedents. (Contributed by Alan Sare, 3-Dec-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses jaoded.1 ( 𝜑 → ( 𝜓𝜒 ) )
jaoded.2 ( 𝜃 → ( 𝜏𝜒 ) )
jaoded.3 ( 𝜂 → ( 𝜓𝜏 ) )
Assertion jaoded ( ( 𝜑𝜃𝜂 ) → 𝜒 )

Proof

Step Hyp Ref Expression
1 jaoded.1 ( 𝜑 → ( 𝜓𝜒 ) )
2 jaoded.2 ( 𝜃 → ( 𝜏𝜒 ) )
3 jaoded.3 ( 𝜂 → ( 𝜓𝜏 ) )
4 jao ( ( 𝜓𝜒 ) → ( ( 𝜏𝜒 ) → ( ( 𝜓𝜏 ) → 𝜒 ) ) )
5 4 3imp ( ( ( 𝜓𝜒 ) ∧ ( 𝜏𝜒 ) ∧ ( 𝜓𝜏 ) ) → 𝜒 )
6 1 2 3 5 syl3an ( ( 𝜑𝜃𝜂 ) → 𝜒 )