Theorem 3anim123i 1190

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 1026	. 2 |- ( ( ph /\ ch /\ ta ) -> ps )
3		3anim123i.2	. . 3 |- ( ch -> th )
4	3	3ad2ant2 1027	. 2 |- ( ( ph /\ ch /\ ta ) -> th )
5		3anim123i.3	. . 3 |- ( ta -> et )
6	5	3ad2ant3 1028	. 2 |- ( ( ph /\ ch /\ ta ) -> et )
7	2, 4, 6	3jca 1185	1 |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )

Syntax hints:   -> wi 4   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  3anim1i  1191  3anim2i  1192  3anim3i  1193  syl3an  1306  syl3anl  1315  spc3egv  3176  eloprabga  6397  le2tri3i  9763  fzmmmeqm  11830  elfz1b  11862  elfz0fzfz0  11893  elfzmlbmOLD  11899  elfzmlbp  11900  elfzo1  11962  ssfzoulel  12002  flltdivnn0lt  12062  swrdswrd  12801  swrdccatin2  12828  swrdccat  12834  mulmoddvds  14341  nndvdslegcd  14453  ncoprmlnprm  14648  symg2hash  16989  pmtrdifellem2  17069  unitgrp  17830  isdrngd  17935  bcthlem5  22189  colinearalg  24786  axcontlem8  24847  usgra2adedgwlk  25187  rngosn  25977  chirredlem2  27879  rexdiv  28233  bnj944  29537  bnj969  29545  nnssi2  30900  nnssi3  30901  isdrngo2  31901  leatb  32567  paddasslem9  33102  paddasslem10  33103  dvhvaddass  34374  expgrowthi  36319  nnsum4primesodd  38281  nnsum4primesoddALTV  38282  2zrngasgrp  38698  2zrngmsgrp  38705  lincvalpr  38971  refdivmptf  39114  refdivmptfv  39118