Description: Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009) (Proof shortened by Andrew Salmon, 13-May-2011) (Proof shortened by Garrett Katz, 16-Jun-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | 3jaao.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 3jaao.2 | |- ( th -> ( ta -> ch ) ) |
||
| 3jaao.3 | |- ( et -> ( ze -> ch ) ) |
||
| Assertion | 3jaao | |- ( ( ph /\ th /\ et ) -> ( ( ps \/ ta \/ ze ) -> ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3jaao.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 2 | 3jaao.2 | |- ( th -> ( ta -> ch ) ) |
|
| 3 | 3jaao.3 | |- ( et -> ( ze -> ch ) ) |
|
| 4 | 3jao | |- ( ( ( ps -> ch ) /\ ( ta -> ch ) /\ ( ze -> ch ) ) -> ( ( ps \/ ta \/ ze ) -> ch ) ) |
|
| 5 | 1 2 3 4 | syl3an | |- ( ( ph /\ th /\ et ) -> ( ( ps \/ ta \/ ze ) -> ch ) ) |