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  4464  fvun1d  5771  fvun2d  5772  funsssuppss  6498  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  ctssdccl  7451  onntri35  7596  dftap2  7617  ltexnqq  7775  enq0tr  7801  prarloc  7870  addclpr  7904  nqprxx  7913  mulclpr  7939  ltexprlempr  7975  recexprlempr  7999  cauappcvgprlemcl  8020  caucvgprlemcl  8043  caucvgprprlemcl  8071  suplocexprlemex  8089  mpomulf  8316  le2tri3i  8435  ltmul1  8922  nn0ge2m1nn  9631  difgtsumgt  9718  nn0ge0div  9737  eluzp1p1  9957  peano2uz  9992  zgt1rpn0n1  10106  ledivge1le  10137  elioc2  10348  elico2  10349  elicc2  10350  iccsupr  10378  elfzd  10429  uzsubsubfz  10462  fzrev3  10504  elfz1b  10507  fseq1p1m1  10511  elfz0ubfz0  10542  elfz0fzfz0  10543  fz0fzelfz0  10544  fz0fzdiffz0  10547  elfzmlbp  10549  elfzo2  10567  elfzo0  10603  nn0p1elfzo  10604  fzo1fzo0n0  10605  elfzo0z  10606  fzofzim  10610  elfzo1  10613  ubmelfzo  10628  elfzodifsumelfzo  10629  elfzom1elp1fzo  10630  fzossfzop1  10640  ssfzo12bi  10653  subfzo0  10671  fldiv4p1lem1div2  10753  intqfrac2  10769  intfracq  10770  modfzo0difsn  10845  iseqf1olemqcl  10949  iseqf1olemnab  10951  iseqf1olemab  10952  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemstep  10964  seqf1oglem2  10970  hashtpg  11313  wrdlenge2n0  11354  ccatval21sw  11387  ccatass  11390  lswccatn0lsw  11393  wrdl1s1  11412  swrdlen2  11448  swrdfv2  11449  swrdspsleq  11453  swrdccat2  11457  pfxnd  11475  swrdswrdlem  11490  swrdpfx  11493  pfxpfx  11494  pfxccatin12lem2a  11513  pfxccatin12lem1  11514  swrdccatin2  11515  pfxccatin12lem2c  11516  pfxccatin12lem2  11517  pfxccatin12lem3  11518  pfxccatin12  11519  pfxccat3  11520  swrdccat  11521  remullem  11650  qdenre  11983  maxabslemval  11989  xrmaxiflemval  12032  summodclem2a  12164  fsum3  12170  fsum3cvg3  12179  fsumcl2lem  12181  fsumadd  12189  sumsplitdc  12215  fsummulc2  12231  isumlessdc  12279  prodmodclem3  12358  prodmodclem2a  12359  prodmodclem2  12360  prodmodc  12361  fprodeq0  12400  sin02gt0  12547  p1modz1  12577  divconjdvds  12632  addmodlteqALT  12642  ltoddhalfle  12676  4dvdseven  12700  dfgcd2  12807  rppwr  12821  qredeq  12890  divgcdcoprmex  12896  cncongr1  12897  dvdsnprmd  12919  oddprmge3  12930  isprm5  12937  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem19  13081  difsqpwdvds  13137  oddprmdvds  13153  ennnfoneleminc  13351  ctinf  13370  ssomct  13385  sgrpidmndm  13782  idmhm  13825  mhmf1o  13826  insubm  13841  0mhm  13842  resmhm  13843  resmhm2  13844  resmhm2b  13845  mhmco  13846  grpinvid1  13906  grpinvid2  13907  grplcan  13916  dfgrp3m  13953  dfgrp3me  13954  mhmfmhm  13969  issubg2m  14041  issubg4m  14045  ghmmhm  14105  rngrz  14294  srglmhm  14346  srgrmhm  14347  ringlz  14397  ringrz  14398  ringinvnzdiv  14404  ring1  14413  unitgrp  14472  isrhm2d  14521  subrgunit  14596  issubrg2  14598  islmodd  14678  dflidl2rng  14867  rnglidlmmgm  14882  quscrng  14919  upxp  15422  bdmopn  15654  suplociccex  15775  ivthreinc  15795  ptolemy  15975  birthdaylem1g  16144  perfectlem1  16197  gausslemma2dlem1a  16275  gausslemma2dlem4  16281  uhgr2edg  16545  umgrvad2edg  16550  uspgredg2vlem  16559  wlkpropg  16663  wlkv  16665  wlkvtxeledgg  16683  upgr2wlkdc  16716  trlsv  16723  clwwlkccat  16740  umgrclwwlkge2  16741  loopclwwlkn1b  16758  clwwlkn1loopb  16759  clwwlkext2edg  16761  s2elclwwlknon2  16775  clwwlknonex2lem2  16777  clwwlknonex2  16778  eupthv  16785  depindlem1  16845  dceqnconst  17208  dcapnconst  17209