Theorem 3jca 1203

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

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

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 1006

This theorem is referenced by:  3jcad  1204  mpbir3and  1206  syl3anbrc  1207  3anim123i  1210  syl3anc  1273  syl13anc  1275  syl31anc  1276  syl113anc  1285  syl131anc  1286  syl311anc  1287  syl33anc  1288  syl133anc  1296  syl313anc  1297  syl331anc  1298  syl333anc  1305  3jaob  1338  mp3and  1376  issod  4416  tfrlemibxssdm  6492  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  ctssdccl  7309  onntri35  7454  dftap2  7469  ltexnqq  7627  enq0tr  7653  prarloc  7722  addclpr  7756  nqprxx  7765  mulclpr  7791  ltexprlempr  7827  recexprlempr  7851  cauappcvgprlemcl  7872  caucvgprlemcl  7895  caucvgprprlemcl  7923  suplocexprlemex  7941  mpomulf  8168  le2tri3i  8287  ltmul1  8771  nn0ge2m1nn  9461  difgtsumgt  9548  nn0ge0div  9566  eluzp1p1  9781  peano2uz  9816  zgt1rpn0n1  9929  ledivge1le  9960  elioc2  10170  elico2  10171  elicc2  10172  iccsupr  10200  elfzd  10250  uzsubsubfz  10281  fzrev3  10321  elfz1b  10324  fseq1p1m1  10328  elfz0ubfz0  10359  elfz0fzfz0  10360  fz0fzelfz0  10361  fz0fzdiffz0  10364  elfzmlbp  10366  elfzo2  10384  elfzo0  10420  fzo1fzo0n0  10421  elfzo0z  10422  fzofzim  10426  elfzo1  10429  ubmelfzo  10444  elfzodifsumelfzo  10445  elfzom1elp1fzo  10446  fzossfzop1  10456  ssfzo12bi  10469  subfzo0  10487  fldiv4p1lem1div2  10564  intqfrac2  10580  intfracq  10581  modfzo0difsn  10656  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemab  10763  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemstep  10775  seqf1oglem2  10781  wrdlenge2n0  11148  ccatval21sw  11181  ccatass  11184  lswccatn0lsw  11187  wrdl1s1  11206  swrdlen2  11242  swrdfv2  11243  swrdspsleq  11247  swrdccat2  11251  pfxnd  11269  swrdswrdlem  11284  swrdpfx  11287  pfxpfx  11288  pfxccatin12lem2a  11307  pfxccatin12lem1  11308  swrdccatin2  11309  pfxccatin12lem2c  11310  pfxccatin12lem2  11311  pfxccatin12lem3  11312  pfxccatin12  11313  pfxccat3  11314  swrdccat  11315  remullem  11431  qdenre  11762  maxabslemval  11768  xrmaxiflemval  11810  summodclem2a  11941  fsum3  11947  fsum3cvg3  11956  fsumcl2lem  11958  fsumadd  11966  sumsplitdc  11992  fsummulc2  12008  isumlessdc  12056  prodmodclem3  12135  prodmodclem2a  12136  prodmodclem2  12137  prodmodc  12138  fprodeq0  12177  sin02gt0  12324  p1modz1  12354  divconjdvds  12409  addmodlteqALT  12419  ltoddhalfle  12453  4dvdseven  12477  dfgcd2  12584  rppwr  12598  qredeq  12667  divgcdcoprmex  12673  cncongr1  12674  dvdsnprmd  12696  oddprmge3  12706  isprm5  12713  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem19  12854  difsqpwdvds  12910  oddprmdvds  12926  ennnfoneleminc  13031  ctinf  13050  ssomct  13065  sgrpidmndm  13502  idmhm  13551  mhmf1o  13552  insubm  13567  0mhm  13568  resmhm  13569  resmhm2  13570  resmhm2b  13571  mhmco  13572  grpinvid1  13634  grpinvid2  13635  grplcan  13644  dfgrp3m  13681  dfgrp3me  13682  mhmfmhm  13703  issubg2m  13775  issubg4m  13779  ghmmhm  13839  rngrz  13958  srglmhm  14005  srgrmhm  14006  ringlz  14055  ringrz  14056  ringinvnzdiv  14062  ring1  14071  unitgrp  14129  isrhm2d  14178  subrgunit  14252  issubrg2  14254  islmodd  14306  dflidl2rng  14494  rnglidlmmgm  14509  quscrng  14546  upxp  14995  bdmopn  15227  suplociccex  15348  ivthreinc  15368  ptolemy  15547  perfectlem1  15722  gausslemma2dlem1a  15786  gausslemma2dlem4  15792  uhgr2edg  16056  umgrvad2edg  16061  uspgredg2vlem  16070  wlkpropg  16174  wlkv  16176  wlkvtxeledgg  16194  upgr2wlkdc  16227  trlsv  16234  clwwlkccat  16251  umgrclwwlkge2  16252  loopclwwlkn1b  16269  clwwlkn1loopb  16270  clwwlkext2edg  16272  s2elclwwlknon2  16286  clwwlknonex2lem2  16288  clwwlknonex2  16289  eupthv  16296  dceqnconst  16664  dcapnconst  16665