Theorem 3jca 1208

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 1011	. 2 |- ( ( ps /\ ch /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
6	4, 5	sylibr 134	1 |- ( ph -> ( ps /\ ch /\ th ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ 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:  3jcad  1209  mpbir3and  1211  syl3anbrc  1212  3anim123i  1215  syl3anc  1278  syl13anc  1280  syl31anc  1281  syl113anc  1290  syl131anc  1291  syl311anc  1292  syl33anc  1293  syl133anc  1301  syl313anc  1302  syl331anc  1303  syl333anc  1310  3jaob  1343  mp3and  1381  issod  4466  fvun1d  5774  fvun2d  5775  funsssuppss  6502  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  ctssdccl  7457  onntri35  7602  dftap2  7623  ltexnqq  7781  enq0tr  7807  prarloc  7876  addclpr  7910  nqprxx  7919  mulclpr  7945  ltexprlempr  7981  recexprlempr  8005  cauappcvgprlemcl  8026  caucvgprlemcl  8049  caucvgprprlemcl  8077  suplocexprlemex  8095  mpomulf  8322  le2tri3i  8441  ltmul1  8928  nn0ge2m1nn  9638  difgtsumgt  9725  nn0ge0div  9744  eluzp1p1  9964  peano2uz  9999  zgt1rpn0n1  10113  ledivge1le  10144  elioc2  10355  elico2  10356  elicc2  10357  iccsupr  10385  elfzd  10436  uzsubsubfz  10469  fzrev3  10511  elfz1b  10514  fseq1p1m1  10518  elfz0ubfz0  10549  elfz0fzfz0  10550  fz0fzelfz0  10551  fz0fzdiffz0  10554  elfzmlbp  10556  elfzo2  10574  elfzo0  10610  nn0p1elfzo  10611  fzo1fzo0n0  10612  elfzo0z  10613  fzofzim  10617  elfzo1  10620  ubmelfzo  10635  elfzodifsumelfzo  10636  elfzom1elp1fzo  10637  fzossfzop1  10647  ssfzo12bi  10660  subfzo0  10678  fldiv4p1lem1div2  10761  intqfrac2  10777  intfracq  10778  modfzo0difsn  10853  iseqf1olemqcl  10957  iseqf1olemnab  10959  iseqf1olemab  10960  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemstep  10972  seqf1oglem2  10978  hashtpg  11321  wrdlenge2n0  11362  ccatval21sw  11395  ccatass  11398  lswccatn0lsw  11401  wrdl1s1  11420  swrdlen2  11456  swrdfv2  11457  swrdspsleq  11461  swrdccat2  11465  pfxnd  11483  swrdswrdlem  11498  swrdpfx  11501  pfxpfx  11502  pfxccatin12lem2a  11521  pfxccatin12lem1  11522  swrdccatin2  11523  pfxccatin12lem2c  11524  pfxccatin12lem2  11525  pfxccatin12lem3  11526  pfxccatin12  11527  pfxccat3  11528  swrdccat  11529  remullem  11658  qdenre  11991  maxabslemval  11997  xrmaxiflemval  12041  summodclem2a  12173  fsum3  12179  fsum3cvg3  12188  fsumcl2lem  12190  fsumadd  12198  sumsplitdc  12224  fsummulc2  12240  isumlessdc  12288  prodmodclem3  12367  prodmodclem2a  12368  prodmodclem2  12369  prodmodc  12370  fprodeq0  12409  sin02gt0  12556  p1modz1  12586  divconjdvds  12641  addmodlteqALT  12651  ltoddhalfle  12685  4dvdseven  12709  dfgcd2  12816  rppwr  12830  qredeq  12899  divgcdcoprmex  12905  cncongr1  12906  dvdsnprmd  12928  oddprmge3  12939  isprm5  12946  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem19  13090  difsqpwdvds  13146  oddprmdvds  13162  ennnfoneleminc  13360  ctinf  13379  ssomct  13394  sgrpidmndm  13792  idmhm  13835  mhmf1o  13836  insubm  13851  0mhm  13852  resmhm  13853  resmhm2  13854  resmhm2b  13855  mhmco  13856  grpinvid1  13916  grpinvid2  13917  grplcan  13926  dfgrp3m  13963  dfgrp3me  13964  mhmfmhm  13979  issubg2m  14051  issubg4m  14055  ghmmhm  14115  rngrz  14352  srglmhm  14404  srgrmhm  14405  ringlz  14455  ringrz  14456  ringinvnzdiv  14462  ring1  14471  unitgrp  14532  isrhm2d  14581  subrgunit  14656  issubrg2  14658  islmodd  14738  dflidl2rng  14927  rnglidlmmgm  14942  quscrng  14979  upxp  15498  bdmopn  15730  suplociccex  15851  ivthreinc  15871  ptolemy  16051  birthdaylem1g  16225  perfectlem1  16299  gausslemma2dlem1a  16382  gausslemma2dlem4  16388  uhgr2edg  16652  umgrvad2edg  16657  uspgredg2vlem  16666  wlkpropg  16770  wlkv  16772  wlkvtxeledgg  16790  upgr2wlkdc  16823  trlsv  16830  clwwlkccat  16847  umgrclwwlkge2  16848  loopclwwlkn1b  16865  clwwlkn1loopb  16866  clwwlkext2edg  16868  s2elclwwlknon2  16882  clwwlknonex2lem2  16884  clwwlknonex2  16885  eupthv  16892  depindlem1  16952  dceqnconst  17317  dcapnconst  17318