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  6175  le2tri3i  8435  fzmmmeqm  10474  elfz1b  10507  elfz0fzfz0  10543  elfzmlbp  10549  elfzo1  10613  flltdivnn0lt  10752  pfxeq  11482  swrdswrd  11491  swrdccat  11521  modmulconst  12606  nndvdslegcd  12758  lgsmulsqcoprm  16263