Theorem jca 306

Description: Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

Ref	Expression
jca.1	|- ( ph -> ps )
jca.2	|- ( ph -> ch )

Assertion

Ref	Expression
jca	|- ( ph -> ( ps /\ ch ) )

Proof of Theorem jca

Step	Hyp	Ref	Expression
1		jca.1	. 2 |- ( ph -> ps )
2		jca.2	. 2 |- ( ph -> ch )
3		pm3.2 139	. 2 |- ( ps -> ( ch -> ( ps /\ ch ) ) )
4	1, 2, 3	sylc 62	1 |- ( ph -> ( ps /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  jca31  309  jca32  310  jcai  311  jctil  312  jctir  313  ancli  323  ancri  324  sylanbrc  417  jcab  603  biadanid  614  ioran  754  ordi  818  stdcndc  847  stdcndcOLD  848  dfandc  886  mpbi2and  946  mpbir2and  947  pm4.82  953  pm4.83dc  954  rnlem  979  syl22anc  1251  syl112anc  1254  syl121anc  1255  syl211anc  1256  syl23anc  1257  syl32anc  1258  syl122anc  1259  syl212anc  1260  syl221anc  1261  syl222anc  1266  syl123anc  1267  syl132anc  1268  syl213anc  1269  syl231anc  1270  syl312anc  1271  syl321anc  1272  syl223anc  1276  syl232anc  1277  syl322anc  1278  syl233anc  1279  syl323anc  1280  syl332anc  1281  ecased  1362  19.26  1504  nfand  1591  19.40  1654  equsexd  1752  sbcof2  1833  sbequ8  1870  eu2  2098  eu3h  2099  eu5  2101  mooran2  2127  datisi  2164  felapton  2168  darapti  2169  dimatis  2171  fresison  2172  fesapo  2174  reximssdv  2610  r19.26  2632  r19.29af2  2646  r19.40  2660  eqvinc  2896  eqvincg  2897  elrabd  2931  reu6  2962  reu3  2963  indifdir  3429  undif3ss  3434  un00  3507  eqifdc  3607  disjpr2  3697  prel12  3812  prneimg  3815  preqsn  3816  disjiun  4040  opth  4282  0nelop  4293  euotd  4300  opelopabsb  4307  ispod  4352  elon2  4424  unexb  4490  opeluu  4498  eusvnfb  4502  suc11g  4606  nlimsucg  4615  tfi  4631  vtoclr  4724  opthprc  4727  ideqg  4830  resiexg  5005  dminss  5098  imainss  5099  ssxpbm  5119  relrelss  5210  funopg  5306  fununfun  5318  fntpg  5331  fun11uni  5345  imain  5357  funimaexglem  5358  funssxp  5447  ffdm  5448  f00  5469  dffo2  5504  fodmrnu  5508  foco  5511  fun11iun  5545  f1o00  5559  fsnd  5567  fv3  5601  dff2  5726  dff3im  5727  dffo4  5730  ffnfv  5740  ffvresb  5745  fsn2  5756  fconstfvm  5804  fnfvima  5821  fcof1o  5860  isocnv  5882  isotr  5887  riotaprop  5925  acexmidlemcase  5941  caovlem2d  6141  f1ocnvd  6150  caofcom  6191  resfunexgALT  6195  elxp7  6258  2ndrn  6271  1stconst  6309  2ndconst  6310  cnvf1olem  6312  poxp  6320  dftpos4  6351  dfsmo2  6375  tfrlem5  6402  tfrlemiex  6419  tfr1onlemsucaccv  6429  tfr1onlembfn  6432  tfr1onlemex  6435  tfr1onlemres  6437  tfrcllemsucaccv  6442  tfrcllembfn  6445  tfrcllemex  6448  tfrcllemres  6450  tfrcl  6452  frecabex  6486  frecabcl  6487  frecfcllem  6492  frecrdg  6496  oawordi  6557  nntri3  6585  nntr2  6591  nnmordi  6604  iserd  6648  relelec  6664  erth  6668  qliftfun  6706  mapsncnv  6784  mptelixpg  6823  bren  6837  pw2f1odclem  6933  findcard2d  6990  findcard2sd  6991  isinfinf  6996  tridc  6998  nnwetri  7015  undifdcss  7022  fiintim  7030  fisseneq  7033  fidcenumlemim  7056  sbthlemi9  7069  supisolem  7112  ordiso2  7139  updjud  7186  difinfsn  7204  ctssdccl  7215  nnnninfeq  7232  omniwomnimkv  7271  acfun  7321  exmidontriimlem2  7336  onntri45  7355  dftap2  7365  netap  7368  2omotaplemap  7371  ccfunen  7378  cc4f  7383  cc4n  7385  elni2  7429  dfplpq2  7469  dfmpq2  7470  enqbreq2  7472  enqdc1  7477  addcmpblnq  7482  addclnq  7490  nqpi  7493  addassnqg  7497  mulassnqg  7499  mulcanenq  7500  distrnqg  7502  1qec  7503  recexnq  7505  subhalfnqq  7529  enq0tr  7549  nqnq0pi  7553  nq0nn  7557  mulcanenq0ec  7560  nnnq0lem1  7561  addclnq0  7566  distrnq0  7574  addassnq0lemcl  7576  elnp1st2nd  7591  prarloc  7618  addlocprlemlt  7646  addlocprlemeq  7648  addlocprlemgt  7649  addclpr  7652  nqprm  7657  mullocprlem  7685  mullocpr  7686  mulclpr  7687  ltpopr  7710  ltaddpr  7712  ltexprlemm  7715  ltexprlemopl  7716  ltexprlemopu  7718  ltexprlemrnd  7720  ltexprlemdisj  7721  addcanprleml  7729  addcanprlemu  7730  addcanprg  7731  recexprlemm  7739  recexprlemopl  7740  recexprlemopu  7742  recexprlemrnd  7744  recexprlemdisj  7745  cauappcvgprlemm  7760  cauappcvgprlemopl  7761  cauappcvgprlemopu  7763  cauappcvgprlemrnd  7765  cauappcvgprlemdisj  7766  cauappcvgprlemlim  7776  caucvgprlemnkj  7781  caucvgprlemm  7783  caucvgprlemopl  7784  caucvgprlemopu  7786  caucvgprlemrnd  7788  caucvgprlemlim  7796  caucvgprprlemnkltj  7804  caucvgprprlemnkeqj  7805  caucvgprprlemnjltk  7806  caucvgprprlemm  7811  caucvgprprlemopl  7812  caucvgprprlemopu  7814  caucvgprprlemrnd  7816  caucvgprprlemexbt  7821  caucvgprprlemlim  7826  suplocexprlemrl  7832  suplocexprlemru  7834  suplocexprlemdisj  7835  suplocexprlemloc  7836  suplocexprlemex  7837  suplocexprlemub  7838  prsrlem1  7857  mulclsr  7869  mulasssrg  7873  distrsrg  7874  suplocsrlemb  7921  elreal2  7945  axmulass  7988  axdistr  7989  axcaucvglemcau  8013  add20  8549  mullt0  8555  rereim  8661  ltmul1  8667  cru  8677  mulap0r  8690  aprcl  8721  aptap  8725  divmuldivap  8787  divmuleqap  8792  divadddivap  8802  divmuldivapd  8907  divmuleqapd  8908  div2subap  8912  ltmul12a  8935  lemul12a  8937  lemulge11  8941  lediv12a  8969  lediv2a  8970  recgt1i  8973  recreclt  8975  ledivp1  8978  lemul1ad  9014  lemul2ad  9015  ltmul12ad  9016  lemul12ad  9017  lemul12bd  9018  nndivre  9074  nndivtr  9080  halfaddsubcl  9272  halfaddsub  9273  lt2halves  9275  nnrecl  9295  elnn0nn  9339  elnnnn0b  9341  elnnnn0c  9342  nn0addge1  9343  nn0addge2  9344  xnn0xrnemnf  9372  elnn0z  9387  elnnz1  9397  nzadd  9427  elz2  9446  zdivadd  9464  zdivmul  9465  zextle  9466  peano2uz2  9482  uzind  9486  btwnz  9494  uzss  9671  eluzp1m1  9674  infregelbex  9721  eluz2b2  9726  qre  9748  qaddcl  9758  qmulcl  9760  qreccl  9765  irradd  9769  irrmul  9770  elpqb  9773  cnref1o  9774  rprege0  9792  rprene0  9795  rpreap0  9796  rpcnne0  9797  rpcnap0  9798  rpregt0d  9827  rprege0d  9828  rprene0d  9829  rpcnne0d  9830  lediv2ad  9843  ledivge1le  9850  lediv12ad  9880  nnledivrp  9890  nn0ledivnn  9891  xrlttri3  9921  xrrebnd  9943  xrrege0  9949  xnn0xadd0  9991  xlesubadd  10007  elioo4g  10058  ioomax  10072  iccmax  10073  divelunit  10126  elfz5  10141  uzsubsubfz  10171  fzopth  10185  fzass4  10186  fzrev2  10209  uzsplit  10216  elfz2nn0  10236  difelfzle  10258  1fv  10263  4fvwrd4  10264  fzo1fzo0n0  10309  elfzom1elp1fzo  10333  subfzo0  10373  infssuzex  10378  qtri3or  10385  adddivflid  10437  flltdivnn0lt  10449  intfracq  10467  modqid2  10498  modfzo0difsn  10542  seq3val  10607  seqvalcd  10608  iseqf1olemqcl  10646  iseqf1olemnab  10648  iseqf1olemab  10649  iseqf1olemmo  10652  seq3f1olemqsumkj  10658  seq3f1olemqsumk  10659  seqf1oglem1  10666  seqf1oglem2  10667  expclzaplem  10710  leexp1a  10741  expubnd  10743  le2sq2  10762  sumsqeq0  10765  bernneq  10807  expnlbnd  10811  nn0opthd  10869  faclbnd6  10891  facavg  10893  seq3coll  10989  hash2en  10990  wrdnval  11026  ccat0  11055  ccatsymb  11061  swrdspsleq  11123  pfxtrcfv  11147  pfxsuffeqwrdeq  11152  shftlem  11160  shftfvalg  11162  shftfval  11165  cvg1nlemcau  11328  cvg1nlemres  11329  rexuz3  11334  resqrexlemcvg  11363  resqrexlemglsq  11366  resqrexlemga  11367  sqrtle  11380  sqrtlt  11381  sqrt11  11383  sqrtsq2  11387  absmul  11413  sqabs  11426  abslt  11432  absle  11433  lenegsq  11439  maxleastb  11558  maxltsup  11562  rexanre  11564  negfi  11572  xrmaxiflemab  11591  xrmaxiflemlub  11592  xrmaxltsup  11602  xrmaxadd  11605  climcn2  11653  mulcn2  11656  summodclem2a  11725  summodc  11727  fsum3  11731  fsum3cvg3  11740  fsumcl2lem  11742  fsumadd  11750  fsump1i  11777  fsum0diaglem  11784  mptfzshft  11786  fsumrev  11787  fsummulc2  11792  fsum00  11806  expcnvap0  11846  mertenslemi1  11879  ntrivcvgap0  11893  prodmodclem3  11919  prodmodclem2a  11920  zproddc  11923  fprodseq  11927  fprodrev  11963  fprodconst  11964  eftlub  12034  efieq  12079  sincos1sgn  12109  demoivreALT  12118  dvdsval3  12135  dvdscmul  12162  dvdsmulc  12163  dvdscmulr  12164  dvdsmulcr  12165  modmulconst  12167  dvds2ln  12168  ltoddhalfle  12237  nn0o  12251  divalg2  12270  ndvdssub  12274  ndvdsadd  12275  divgcdz  12325  gcd0id  12333  gcdaddm  12338  bezoutlemstep  12351  bezoutlemmain  12352  dfgcd3  12364  dfgcd2  12368  lcmcllem  12422  dvdslcm  12424  lcmgcdlem  12432  lcmgcdnn  12437  qredeq  12451  qredeu  12452  rpdvds  12454  divgcdcoprm0  12456  cncongr1  12458  cncongr2  12459  cncongrcoprm  12461  prmind2  12475  isprm5  12497  isprm6  12502  prmexpb  12506  cncongrprm  12512  sqrt2irrlem  12516  pw2dvdslemn  12520  oddpwdclemxy  12524  oddpwdclemdc  12528  oddpwdc  12529  hashdvds  12576  prmdiv  12590  hashgcdlem  12593  nnoddn2prmb  12618  pythagtriplem6  12626  pythagtriplem7  12627  pcpre1  12648  pccl  12655  pcmul  12657  pcdiv  12658  pcqmul  12659  pcqcl  12662  pcdvds  12671  pcndvds  12673  pcndvds2  12675  pc2dvds  12686  dvdsprmpweqle  12693  difsqpwdvds  12694  pcaddlem  12695  pcadd  12696  pcmptcl  12698  pcmpt  12699  fldivp1  12704  pcfac  12706  oddprmdvds  12710  infpnlem2  12716  4sqlem5  12738  4sqlem6  12739  4sqlem4a  12747  4sqexercise1  12754  4sqexercise2  12755  4sqlem13m  12759  4sqlem15  12761  4sqlem16  12762  ennnfonelemfun  12821  ennnfonelemim  12828  ctinfomlemom  12831  ctinfom  12832  ctinf  12834  ctiunctlemfo  12843  omctfn  12847  fnpr2ob  13205  ismgmid2  13245  fngsum  13253  igsumvalx  13254  gsumfzval  13256  gsum0g  13261  gsumval2  13262  issgrpd  13277  ismndd  13302  prdsidlem  13312  imasmnd2  13317  mhmf1o  13335  subsubm  13348  dfgrp2  13392  isgrpid2  13405  isgrpinv  13419  grplrinv  13422  dfgrp3mlem  13463  dfgrp3m  13464  dfgrp3me  13465  prdsinvlem  13473  imasgrp2  13479  mhmmnd  13485  issubg2m  13558  issubgrpd2  13559  grpissubg  13563  subsubg  13566  subgintm  13567  isnsg3  13576  nmzsubg  13579  eqgval  13592  eqgen  13596  isghmd  13621  ghmrn  13626  ghmpreima  13635  ghmf1o  13644  conjghm  13645  conjnmzb  13649  ghmpropd  13652  rinvmod  13678  imasabl  13705  rnglz  13740  isrngd  13748  srgdilem  13764  srglmhm  13788  srgrmhm  13789  ringdilem  13807  isringd  13836  ringsrg  13842  ringinvnzdiv  13845  imasring  13859  dvdsrd  13889  unitgrp  13911  isrim0  13956  isrhm2d  13960  rhmf1o  13963  rhmco  13969  rhmopp  13971  issubrng2  14005  subsubrng  14009  subrgugrp  14035  issubrg2  14036  subsubrg  14040  resrhm  14043  aprap  14081  lmodfopnelem2  14120  lsssubg  14172  islss3  14174  islss4  14177  lspsnel6  14203  lidlacl  14279  lidlsubg  14281  lidlrsppropdg  14290  2idlelbas  14311  cnfld1  14367  cnsubglem  14374  mulgghm2  14403  zndvds  14444  mplsubgfi  14496  topgele  14534  tgcl  14569  epttop  14595  opnssneib  14661  iscnp4  14723  cnco  14726  cncnp  14735  cnrest2  14741  lmss  14751  txcnp  14776  txcn  14780  cnmpt12  14792  cnmpt22  14799  hmeof1o  14814  psmetres2  14838  distspace  14840  ismeti  14851  isxmetd  14852  xmetpsmet  14874  xblss2ps  14909  xblss2  14910  blcntrps  14920  blcntr  14921  blin2  14937  mopni3  14989  metequiv2  15001  bdmet  15007  xmettx  15015  cnbl0  15039  cnblcld  15040  tgioo  15059  elcncf1di  15084  dedekindeulemlu  15126  suplociccex  15130  dedekindicclemlu  15135  dedekindicc  15138  ivthinclemlopn  15141  ivthdec  15149  ivthreinc  15150  ivthdichlem  15156  cnplimcim  15172  limccnp2lem  15181  dvfvalap  15186  plymullem  15255  reeff1olem  15276  sin0pilem1  15286  pilem3  15288  ptolemy  15329  sincosq1sgn  15331  sinq12gt0  15335  ioocosf1o  15359  rprelogbmulexp  15461  perfectlem2  15505  lgslem3  15512  lgsne0  15548  gausslemma2dlem0b  15560  gausslemma2dlem0c  15561  lgsquadlem2  15588  lgsquad2lem2  15592  2lgsoddprmlem2  15616  2sqlem8  15633  gropd  15677  grstructd2dom  15678  bj-nnan  15709  bj-charfun  15780  bdop  15848  bdunexb  15893  bj-om  15910  findset  15918  bj-peano4  15928  bj-inf2vn  15947  bj-inf2vn2  15948  pwle2  15972  pwf1oexmid  15973  nnnninfex  15996  sbthom  16002  qdencn  16003  trilpolemlt1  16017