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  8434  fzmmmeqm  10464  elfz1b  10497  elfz0fzfz0  10533  elfzmlbp  10539  elfzo1  10603  flltdivnn0lt  10739  pfxeq  11468  swrdswrd  11477  swrdccat  11507  modmulconst  12590  nndvdslegcd  12742  lgsmulsqcoprm  16165