Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alan Sare
Conventional Metamath proofs, some derived from VD proofs
jaoded
Metamath Proof Explorer
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
⊢ ( ( 𝜑 ∧ 𝜃 ∧ 𝜂 ) → 𝜒 )