Theorem 3jca 1204

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

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

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 1007

This theorem is referenced by:  3jcad  1205  mpbir3and  1207  syl3anbrc  1208  3anim123i  1211  syl3anc  1274  syl13anc  1276  syl31anc  1277  syl113anc  1286  syl131anc  1287  syl311anc  1288  syl33anc  1289  syl133anc  1297  syl313anc  1298  syl331anc  1299  syl333anc  1306  3jaob  1339  mp3and  1377  issod  4445  funsssuppss  6471  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  ctssdccl  7415  onntri35  7560  dftap2  7581  ltexnqq  7739  enq0tr  7765  prarloc  7834  addclpr  7868  nqprxx  7877  mulclpr  7903  ltexprlempr  7939  recexprlempr  7963  cauappcvgprlemcl  7984  caucvgprlemcl  8007  caucvgprprlemcl  8035  suplocexprlemex  8053  mpomulf  8280  le2tri3i  8398  ltmul1  8883  nn0ge2m1nn  9577  difgtsumgt  9664  nn0ge0div  9683  eluzp1p1  9898  peano2uz  9933  zgt1rpn0n1  10046  ledivge1le  10077  elioc2  10288  elico2  10289  elicc2  10290  iccsupr  10318  elfzd  10369  uzsubsubfz  10401  fzrev3  10443  elfz1b  10446  fseq1p1m1  10450  elfz0ubfz0  10481  elfz0fzfz0  10482  fz0fzelfz0  10483  fz0fzdiffz0  10486  elfzmlbp  10488  elfzo2  10506  elfzo0  10542  nn0p1elfzo  10543  fzo1fzo0n0  10544  elfzo0z  10545  fzofzim  10549  elfzo1  10552  ubmelfzo  10567  elfzodifsumelfzo  10568  elfzom1elp1fzo  10569  fzossfzop1  10579  ssfzo12bi  10592  subfzo0  10610  fldiv4p1lem1div2  10689  intqfrac2  10705  intfracq  10706  modfzo0difsn  10781  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemab  10888  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemstep  10900  seqf1oglem2  10906  hashtpg  11244  wrdlenge2n0  11285  ccatval21sw  11318  ccatass  11321  lswccatn0lsw  11324  wrdl1s1  11343  swrdlen2  11379  swrdfv2  11380  swrdspsleq  11384  swrdccat2  11388  pfxnd  11406  swrdswrdlem  11421  swrdpfx  11424  pfxpfx  11425  pfxccatin12lem2a  11444  pfxccatin12lem1  11445  swrdccatin2  11446  pfxccatin12lem2c  11447  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccatin12  11450  pfxccat3  11451  swrdccat  11452  remullem  11581  qdenre  11912  maxabslemval  11918  xrmaxiflemval  11960  summodclem2a  12092  fsum3  12098  fsum3cvg3  12107  fsumcl2lem  12109  fsumadd  12117  sumsplitdc  12143  fsummulc2  12159  isumlessdc  12207  prodmodclem3  12286  prodmodclem2a  12287  prodmodclem2  12288  prodmodc  12289  fprodeq0  12328  sin02gt0  12475  p1modz1  12505  divconjdvds  12560  addmodlteqALT  12570  ltoddhalfle  12604  4dvdseven  12628  dfgcd2  12735  rppwr  12749  qredeq  12818  divgcdcoprmex  12824  cncongr1  12825  dvdsnprmd  12847  oddprmge3  12857  isprm5  12864  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem19  13005  difsqpwdvds  13061  oddprmdvds  13077  ennnfoneleminc  13246  ctinf  13265  ssomct  13280  sgrpidmndm  13681  idmhm  13724  mhmf1o  13725  insubm  13740  0mhm  13741  resmhm  13742  resmhm2  13743  resmhm2b  13744  mhmco  13745  grpinvid1  13807  grpinvid2  13808  grplcan  13817  dfgrp3m  13854  dfgrp3me  13855  mhmfmhm  13870  issubg2m  13942  issubg4m  13946  ghmmhm  14006  rngrz  14185  srglmhm  14236  srgrmhm  14237  ringlz  14286  ringrz  14287  ringinvnzdiv  14293  ring1  14302  unitgrp  14361  isrhm2d  14410  subrgunit  14485  issubrg2  14487  islmodd  14567  dflidl2rng  14755  rnglidlmmgm  14770  quscrng  14807  upxp  15263  bdmopn  15495  suplociccex  15616  ivthreinc  15636  ptolemy  15815  perfectlem1  15993  gausslemma2dlem1a  16057  gausslemma2dlem4  16063  uhgr2edg  16327  umgrvad2edg  16332  uspgredg2vlem  16341  wlkpropg  16445  wlkv  16447  wlkvtxeledgg  16465  upgr2wlkdc  16498  trlsv  16505  clwwlkccat  16522  umgrclwwlkge2  16523  loopclwwlkn1b  16540  clwwlkn1loopb  16541  clwwlkext2edg  16543  s2elclwwlknon2  16557  clwwlknonex2lem2  16559  clwwlknonex2  16560  eupthv  16567  depindlem1  16627  dceqnconst  16972  dcapnconst  16973