Theorem 3anim123i 1139

Description: Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)

Hypotheses

Ref	Expression
3anim123i.1	|- ( ph -> ps )
3anim123i.2	|- ( ch -> th )
3anim123i.3	|- ( ta -> et )

Assertion

Ref	Expression
3anim123i	|- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )

Proof of Theorem 3anim123i

Step	Hyp	Ref	Expression
1		3anim123i.1	. . 3 |- ( ph -> ps )
2	1	3ad2ant1 978	. 2 |- ( ( ph /\ ch /\ ta ) -> ps )
3		3anim123i.2	. . 3 |- ( ch -> th )
4	3	3ad2ant2 979	. 2 |- ( ( ph /\ ch /\ ta ) -> th )
5		3anim123i.3	. . 3 |- ( ta -> et )
6	5	3ad2ant3 980	. 2 |- ( ( ph /\ ch /\ ta ) -> et )
7	2, 4, 6	3jca 1134	1 |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )

Syntax hints:   -> wi 4   /\ w3a 936

This theorem is referenced by:  3anim1i  1140  3anim3i  1141  syl3an  1226  syl3anl  1235  spc3egv  3000  eloprabga  6119  le2tri3i  9159  elfzo1  11128  unitgrp  15727  isdrngd  15815  bcthlem5  19234  rngosn  21945  chirredlem2  23847  rexdiv  24125  colinearalg  25753  axcontlem8  25814  nnssi2  26109  nnssi3  26110  welb  26328  isdrngo2  26464  expgrowthi  27418  elfzmlbm  27977  elfzmlbp  27978  swrd0swrd  28009  swrdswrd  28011  swrdccatin2  28018  swrdccatin12lem3  28024  usgra2adedgwlk  28046  bnj944  29015  bnj969  29023  leatb  29775  paddasslem9  30310  paddasslem10  30311  dvhvaddass  31580

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938