Theorem 3anim123i 1215

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 1049	. 2 |- ( ( ph /\ ch /\ ta ) -> ps )
3		3anim123i.2	. . 3 |- ( ch -> th )
4	3	3ad2ant2 1050	. 2 |- ( ( ph /\ ch /\ ta ) -> th )
5		3anim123i.3	. . 3 |- ( ta -> et )
6	5	3ad2ant3 1051	. 2 |- ( ( ph /\ ch /\ ta ) -> et )
7	2, 4, 6	3jca 1208	1 |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anim1i  1216  3anim2i  1217  3anim3i  1218  syl3an  1320  syl3anl  1329  spc3egv  2917  spc3gv  2918  eloprabga  6178  le2tri3i  8441  fzmmmeqm  10480  elfz1b  10513  elfz0fzfz0  10549  elfzmlbp  10555  elfzo1  10619  flltdivnn0lt  10759  pfxeq  11489  swrdswrd  11498  swrdccat  11528  modmulconst  12614  nndvdslegcd  12766  lgsmulsqcoprm  16387