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 ) |
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 ) |