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
|- ( ph -> ( ps -> ch ) )
jaoded.2
|- ( th -> ( ta -> ch ) )
jaoded.3
|- ( et -> ( ps \/ ta ) )
Assertion jaoded
|- ( ( ph /\ th /\ et ) -> ch )

Proof

Step Hyp Ref Expression
1 jaoded.1
 |-  ( ph -> ( ps -> ch ) )
2 jaoded.2
 |-  ( th -> ( ta -> ch ) )
3 jaoded.3
 |-  ( et -> ( ps \/ ta ) )
4 jao
 |-  ( ( ps -> ch ) -> ( ( ta -> ch ) -> ( ( ps \/ ta ) -> ch ) ) )
5 4 3imp
 |-  ( ( ( ps -> ch ) /\ ( ta -> ch ) /\ ( ps \/ ta ) ) -> ch )
6 1 2 3 5 syl3an
 |-  ( ( ph /\ th /\ et ) -> ch )