Theorem 3jca 1201

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

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

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 1004

This theorem is referenced by:  3jcad  1202  mpbir3and  1204  syl3anbrc  1205  3anim123i  1208  syl3anc  1271  syl13anc  1273  syl31anc  1274  syl113anc  1283  syl131anc  1284  syl311anc  1285  syl33anc  1286  syl133anc  1294  syl313anc  1295  syl331anc  1296  syl333anc  1303  3jaob  1336  mp3and  1374  issod  4411  tfrlemibxssdm  6484  tfr1onlembxssdm  6500  tfrcllembxssdm  6513  ctssdccl  7294  onntri35  7438  dftap2  7453  ltexnqq  7611  enq0tr  7637  prarloc  7706  addclpr  7740  nqprxx  7749  mulclpr  7775  ltexprlempr  7811  recexprlempr  7835  cauappcvgprlemcl  7856  caucvgprlemcl  7879  caucvgprprlemcl  7907  suplocexprlemex  7925  mpomulf  8152  le2tri3i  8271  ltmul1  8755  nn0ge2m1nn  9445  difgtsumgt  9532  nn0ge0div  9550  eluzp1p1  9765  peano2uz  9795  zgt1rpn0n1  9908  ledivge1le  9939  elioc2  10149  elico2  10150  elicc2  10151  iccsupr  10179  elfzd  10229  uzsubsubfz  10260  fzrev3  10300  elfz1b  10303  fseq1p1m1  10307  elfz0ubfz0  10338  elfz0fzfz0  10339  fz0fzelfz0  10340  fz0fzdiffz0  10343  elfzmlbp  10345  elfzo2  10363  elfzo0  10399  fzo1fzo0n0  10400  elfzo0z  10401  fzofzim  10405  elfzo1  10408  ubmelfzo  10423  elfzodifsumelfzo  10424  elfzom1elp1fzo  10425  fzossfzop1  10435  ssfzo12bi  10448  subfzo0  10465  fldiv4p1lem1div2  10542  intqfrac2  10558  intfracq  10559  modfzo0difsn  10634  iseqf1olemqcl  10738  iseqf1olemnab  10740  iseqf1olemab  10741  seq3f1olemqsumkj  10750  seq3f1olemqsumk  10751  seq3f1olemstep  10753  seqf1oglem2  10759  wrdlenge2n0  11125  ccatval21sw  11158  ccatass  11161  lswccatn0lsw  11164  wrdl1s1  11183  swrdlen2  11215  swrdfv2  11216  swrdspsleq  11220  swrdccat2  11224  pfxnd  11242  swrdswrdlem  11257  swrdpfx  11260  pfxpfx  11261  pfxccatin12lem2a  11280  pfxccatin12lem1  11281  swrdccatin2  11282  pfxccatin12lem2c  11283  pfxccatin12lem2  11284  pfxccatin12lem3  11285  pfxccatin12  11286  pfxccat3  11287  swrdccat  11288  remullem  11403  qdenre  11734  maxabslemval  11740  xrmaxiflemval  11782  summodclem2a  11913  fsum3  11919  fsum3cvg3  11928  fsumcl2lem  11930  fsumadd  11938  sumsplitdc  11964  fsummulc2  11980  isumlessdc  12028  prodmodclem3  12107  prodmodclem2a  12108  prodmodclem2  12109  prodmodc  12110  fprodeq0  12149  sin02gt0  12296  p1modz1  12326  divconjdvds  12381  addmodlteqALT  12391  ltoddhalfle  12425  4dvdseven  12449  dfgcd2  12556  rppwr  12570  qredeq  12639  divgcdcoprmex  12645  cncongr1  12646  dvdsnprmd  12668  oddprmge3  12678  isprm5  12685  pythagtriplem6  12814  pythagtriplem7  12815  pythagtriplem19  12826  difsqpwdvds  12882  oddprmdvds  12898  ennnfoneleminc  13003  ctinf  13022  ssomct  13037  sgrpidmndm  13474  idmhm  13523  mhmf1o  13524  insubm  13539  0mhm  13540  resmhm  13541  resmhm2  13542  resmhm2b  13543  mhmco  13544  grpinvid1  13606  grpinvid2  13607  grplcan  13616  dfgrp3m  13653  dfgrp3me  13654  mhmfmhm  13675  issubg2m  13747  issubg4m  13751  ghmmhm  13811  rngrz  13930  srglmhm  13977  srgrmhm  13978  ringlz  14027  ringrz  14028  ringinvnzdiv  14034  ring1  14043  unitgrp  14101  isrhm2d  14150  subrgunit  14224  issubrg2  14226  islmodd  14278  dflidl2rng  14466  rnglidlmmgm  14481  quscrng  14518  upxp  14967  bdmopn  15199  suplociccex  15320  ivthreinc  15340  ptolemy  15519  perfectlem1  15694  gausslemma2dlem1a  15758  gausslemma2dlem4  15764  uhgr2edg  16025  umgrvad2edg  16030  uspgredg2vlem  16039  wlkpropg  16096  wlkv  16098  wlkvtxeledgg  16116  upgr2wlkdc  16147  trlsv  16154  clwwlkccat  16170  umgrclwwlkge2  16171  loopclwwlkn1b  16187  clwwlkn1loopb  16188  clwwlkext2edg  16190  dceqnconst  16542  dcapnconst  16543