Theorem 3jca 1180

Description: Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)

Hypotheses

Ref	Expression
3jca.1	|- ( ph -> ps )
3jca.2	|- ( ph -> ch )
3jca.3	|- ( ph -> th )

Assertion

Ref	Expression
3jca	|- ( ph -> ( ps /\ ch /\ th ) )

Proof of Theorem 3jca

Step	Hyp	Ref	Expression
1		3jca.1	. . 3 |- ( ph -> ps )
2		3jca.2	. . 3 |- ( ph -> ch )
3		3jca.3	. . 3 |- ( ph -> th )
4	1, 2, 3	jca31 309	. 2 |- ( ph -> ( ( ps /\ ch ) /\ th ) )
5		df-3an 983	. 2 |- ( ( ps /\ ch /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
6	4, 5	sylibr 134	1 |- ( ph -> ( ps /\ ch /\ th ) )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  3jcad  1181  mpbir3and  1183  syl3anbrc  1184  3anim123i  1187  syl3anc  1250  syl13anc  1252  syl31anc  1253  syl113anc  1262  syl131anc  1263  syl311anc  1264  syl33anc  1265  syl133anc  1273  syl313anc  1274  syl331anc  1275  syl333anc  1282  3jaob  1315  mp3and  1353  issod  4367  tfrlemibxssdm  6415  tfr1onlembxssdm  6431  tfrcllembxssdm  6444  ctssdccl  7215  onntri35  7351  dftap2  7365  ltexnqq  7523  enq0tr  7549  prarloc  7618  addclpr  7652  nqprxx  7661  mulclpr  7687  ltexprlempr  7723  recexprlempr  7747  cauappcvgprlemcl  7768  caucvgprlemcl  7791  caucvgprprlemcl  7819  suplocexprlemex  7837  mpomulf  8064  le2tri3i  8183  ltmul1  8667  nn0ge2m1nn  9357  difgtsumgt  9444  nn0ge0div  9462  eluzp1p1  9676  peano2uz  9706  zgt1rpn0n1  9819  ledivge1le  9850  elioc2  10060  elico2  10061  elicc2  10062  iccsupr  10090  elfzd  10140  uzsubsubfz  10171  fzrev3  10211  elfz1b  10214  fseq1p1m1  10218  elfz0ubfz0  10249  elfz0fzfz0  10250  fz0fzelfz0  10251  fz0fzdiffz0  10254  elfzmlbp  10256  elfzo2  10274  elfzo0  10308  fzo1fzo0n0  10309  elfzo0z  10310  fzofzim  10314  elfzo1  10316  ubmelfzo  10331  elfzodifsumelfzo  10332  elfzom1elp1fzo  10333  fzossfzop1  10343  ssfzo12bi  10356  subfzo0  10373  fldiv4p1lem1div2  10450  intqfrac2  10466  intfracq  10467  modfzo0difsn  10542  iseqf1olemqcl  10646  iseqf1olemnab  10648  iseqf1olemab  10649  seq3f1olemqsumkj  10658  seq3f1olemqsumk  10659  seq3f1olemstep  10661  seqf1oglem2  10667  wrdlenge2n0  11031  ccatval21sw  11064  ccatass  11067  lswccatn0lsw  11070  wrdl1s1  11087  swrdlen2  11118  swrdfv2  11119  swrdspsleq  11123  swrdccat2  11127  pfxnd  11143  remullem  11215  qdenre  11546  maxabslemval  11552  xrmaxiflemval  11594  summodclem2a  11725  fsum3  11731  fsum3cvg3  11740  fsumcl2lem  11742  fsumadd  11750  sumsplitdc  11776  fsummulc2  11792  isumlessdc  11840  prodmodclem3  11919  prodmodclem2a  11920  prodmodclem2  11921  prodmodc  11922  fprodeq0  11961  sin02gt0  12108  p1modz1  12138  divconjdvds  12193  addmodlteqALT  12203  ltoddhalfle  12237  4dvdseven  12261  dfgcd2  12368  rppwr  12382  qredeq  12451  divgcdcoprmex  12457  cncongr1  12458  dvdsnprmd  12480  oddprmge3  12490  isprm5  12497  pythagtriplem6  12626  pythagtriplem7  12627  pythagtriplem19  12638  difsqpwdvds  12694  oddprmdvds  12710  ennnfoneleminc  12815  ctinf  12834  ssomct  12849  sgrpidmndm  13285  idmhm  13334  mhmf1o  13335  insubm  13350  0mhm  13351  resmhm  13352  resmhm2  13353  resmhm2b  13354  mhmco  13355  grpinvid1  13417  grpinvid2  13418  grplcan  13427  dfgrp3m  13464  dfgrp3me  13465  mhmfmhm  13486  issubg2m  13558  issubg4m  13562  ghmmhm  13622  rngrz  13741  srglmhm  13788  srgrmhm  13789  ringlz  13838  ringrz  13839  ringinvnzdiv  13845  ring1  13854  unitgrp  13911  isrhm2d  13960  subrgunit  14034  issubrg2  14036  islmodd  14088  dflidl2rng  14276  rnglidlmmgm  14291  quscrng  14328  upxp  14777  bdmopn  15009  suplociccex  15130  ivthreinc  15150  ptolemy  15329  perfectlem1  15504  gausslemma2dlem1a  15568  gausslemma2dlem4  15574  dceqnconst  16036  dcapnconst  16037