Theorem 3anim123i 1173

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 1009	. 2 |- ( ( ph /\ ch /\ ta ) -> ps )
3		3anim123i.2	. . 3 |- ( ch -> th )
4	3	3ad2ant2 1010	. 2 |- ( ( ph /\ ch /\ ta ) -> th )
5		3anim123i.3	. . 3 |- ( ta -> et )
6	5	3ad2ant3 1011	. 2 |- ( ( ph /\ ch /\ ta ) -> et )
7	2, 4, 6	3jca 1168	1 |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )

Syntax hints:   -> wi 4   /\ w3a 965

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967

This theorem is referenced by:  3anim1i  1174  3anim3i  1175  syl3an  1260  syl3anl  1269  spc3egv  3061  eloprabga  6177  le2tri3i  9504  uzletr  10869  elfz0fzfz0  11485  elfzmlbm  11490  elfzmlbp  11491  fzmmmeqm  11492  elfz1b  11527  elfzo0z  11589  elfzo1  11595  ssfzoulel  11621  flltdivnn0lt  11677  swrdspsleq  12342  swrdswrd  12354  swrdccatin2  12378  swrdccat  12384  symg2hash  15902  pmtrdifellem2  15983  unitgrp  16759  isdrngd  16857  mdetunilem9  18426  bcthlem5  20839  colinearalg  23156  axcontlem8  23217  rngosn  23891  chirredlem2  25795  rexdiv  26101  nnssi2  28301  nnssi3  28302  welb  28630  isdrngo2  28764  expgrowthi  29607  uzuzle  30190  el2fzo  30212  mulmoddvds  30246  usgra2adedgwlk  30306  lincvalpr  30952  bnj944  31931  bnj969  31939  leatb  32937  paddasslem9  33472  paddasslem10  33473  dvhvaddass  34742