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)
| 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 | 1 | 3ad2ant1 | |- ( ( ph /\ th /\ et ) -> ( ps -> ch ) ) |
| 5 | 2 | 3ad2ant2 | |- ( ( ph /\ th /\ et ) -> ( ta -> ch ) ) |
| 6 | 3 | 3ad2ant3 | |- ( ( ph /\ th /\ et ) -> ( ze -> ch ) ) |
| 7 | 4 5 6 | 3jaod | |- ( ( ph /\ th /\ et ) -> ( ( ps \/ ta \/ ze ) -> ch ) ) |