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  4442  funsssuppss  6460  tfrlemibxssdm  6560  tfr1onlembxssdm  6576  tfrcllembxssdm  6589  ctssdccl  7404  onntri35  7549  dftap2  7567  ltexnqq  7725  enq0tr  7751  prarloc  7820  addclpr  7854  nqprxx  7863  mulclpr  7889  ltexprlempr  7925  recexprlempr  7949  cauappcvgprlemcl  7970  caucvgprlemcl  7993  caucvgprprlemcl  8021  suplocexprlemex  8039  mpomulf  8266  le2tri3i  8384  ltmul1  8868  nn0ge2m1nn  9562  difgtsumgt  9649  nn0ge0div  9668  eluzp1p1  9883  peano2uz  9918  zgt1rpn0n1  10031  ledivge1le  10062  elioc2  10272  elico2  10273  elicc2  10274  iccsupr  10302  elfzd  10353  uzsubsubfz  10384  fzrev3  10425  elfz1b  10428  fseq1p1m1  10432  elfz0ubfz0  10463  elfz0fzfz0  10464  fz0fzelfz0  10465  fz0fzdiffz0  10468  elfzmlbp  10470  elfzo2  10488  elfzo0  10524  nn0p1elfzo  10525  fzo1fzo0n0  10526  elfzo0z  10527  fzofzim  10531  elfzo1  10534  ubmelfzo  10549  elfzodifsumelfzo  10550  elfzom1elp1fzo  10551  fzossfzop1  10561  ssfzo12bi  10574  subfzo0  10592  fldiv4p1lem1div2  10669  intqfrac2  10685  intfracq  10686  modfzo0difsn  10761  iseqf1olemqcl  10865  iseqf1olemnab  10867  iseqf1olemab  10868  seq3f1olemqsumkj  10877  seq3f1olemqsumk  10878  seq3f1olemstep  10880  seqf1oglem2  10886  hashtpg  11223  wrdlenge2n0  11264  ccatval21sw  11297  ccatass  11300  lswccatn0lsw  11303  wrdl1s1  11322  swrdlen2  11358  swrdfv2  11359  swrdspsleq  11363  swrdccat2  11367  pfxnd  11385  swrdswrdlem  11400  swrdpfx  11403  pfxpfx  11404  pfxccatin12lem2a  11423  pfxccatin12lem1  11424  swrdccatin2  11425  pfxccatin12lem2c  11426  pfxccatin12lem2  11427  pfxccatin12lem3  11428  pfxccatin12  11429  pfxccat3  11430  swrdccat  11431  remullem  11560  qdenre  11891  maxabslemval  11897  xrmaxiflemval  11939  summodclem2a  12071  fsum3  12077  fsum3cvg3  12086  fsumcl2lem  12088  fsumadd  12096  sumsplitdc  12122  fsummulc2  12138  isumlessdc  12186  prodmodclem3  12265  prodmodclem2a  12266  prodmodclem2  12267  prodmodc  12268  fprodeq0  12307  sin02gt0  12454  p1modz1  12484  divconjdvds  12539  addmodlteqALT  12549  ltoddhalfle  12583  4dvdseven  12607  dfgcd2  12714  rppwr  12728  qredeq  12797  divgcdcoprmex  12803  cncongr1  12804  dvdsnprmd  12826  oddprmge3  12836  isprm5  12843  pythagtriplem6  12972  pythagtriplem7  12973  pythagtriplem19  12984  difsqpwdvds  13040  oddprmdvds  13056  ennnfoneleminc  13179  ctinf  13198  ssomct  13213  sgrpidmndm  13650  idmhm  13699  mhmf1o  13700  insubm  13715  0mhm  13716  resmhm  13717  resmhm2  13718  resmhm2b  13719  mhmco  13720  grpinvid1  13782  grpinvid2  13783  grplcan  13792  dfgrp3m  13829  dfgrp3me  13830  mhmfmhm  13851  issubg2m  13923  issubg4m  13927  ghmmhm  13987  rngrz  14107  srglmhm  14154  srgrmhm  14155  ringlz  14204  ringrz  14205  ringinvnzdiv  14211  ring1  14220  unitgrp  14278  isrhm2d  14327  subrgunit  14401  issubrg2  14403  islmodd  14458  dflidl2rng  14646  rnglidlmmgm  14661  quscrng  14698  upxp  15154  bdmopn  15386  suplociccex  15507  ivthreinc  15527  ptolemy  15706  perfectlem1  15884  gausslemma2dlem1a  15948  gausslemma2dlem4  15954  uhgr2edg  16218  umgrvad2edg  16223  uspgredg2vlem  16232  wlkpropg  16336  wlkv  16338  wlkvtxeledgg  16356  upgr2wlkdc  16389  trlsv  16396  clwwlkccat  16413  umgrclwwlkge2  16414  loopclwwlkn1b  16431  clwwlkn1loopb  16432  clwwlkext2edg  16434  s2elclwwlknon2  16448  clwwlknonex2lem2  16450  clwwlknonex2  16451  eupthv  16458  depindlem1  16518  dceqnconst  16863  dcapnconst  16864