Description: Obsolete version of 3jaao as of 16-Jun-2026. 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 modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | 3jaao.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 3jaao.2 | |- ( th -> ( ta -> ch ) ) |
||
| 3jaao.3 | |- ( et -> ( ze -> ch ) ) |
||
| Assertion | 3jaaoOLD | |- ( ( 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 ) ) |