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  753  ordi  817  stdcndc  846  stdcndcOLD  847  dfandc  885  mpbi2and  945  mpbir2and  946  pm4.82  952  pm4.83dc  953  rnlem  978  syl22anc  1250  syl112anc  1253  syl121anc  1254  syl211anc  1255  syl23anc  1256  syl32anc  1257  syl122anc  1258  syl212anc  1259  syl221anc  1260  syl222anc  1265  syl123anc  1266  syl132anc  1267  syl213anc  1268  syl231anc  1269  syl312anc  1270  syl321anc  1271  syl223anc  1275  syl232anc  1276  syl322anc  1277  syl233anc  1278  syl323anc  1279  syl332anc  1280  ecased  1360  19.26  1495  nfand  1582  19.40  1645  equsexd  1743  sbcof2  1824  sbequ8  1861  eu2  2089  eu3h  2090  eu5  2092  mooran2  2118  datisi  2155  felapton  2159  darapti  2160  dimatis  2162  fresison  2163  fesapo  2165  reximssdv  2601  r19.26  2623  r19.29af2  2637  r19.40  2651  eqvinc  2887  eqvincg  2888  elrabd  2922  reu6  2953  reu3  2954  indifdir  3420  undif3ss  3425  un00  3498  eqifdc  3597  disjpr2  3687  prel12  3802  prneimg  3805  preqsn  3806  disjiun  4029  opth  4271  0nelop  4282  euotd  4288  opelopabsb  4295  ispod  4340  elon2  4412  unexb  4478  opeluu  4486  eusvnfb  4490  suc11g  4594  nlimsucg  4603  tfi  4619  vtoclr  4712  opthprc  4715  ideqg  4818  resiexg  4992  dminss  5085  imainss  5086  ssxpbm  5106  relrelss  5197  funopg  5293  fntpg  5315  fun11uni  5329  imain  5341  funimaexglem  5342  funssxp  5430  ffdm  5431  f00  5452  dffo2  5487  fodmrnu  5491  foco  5494  fun11iun  5528  f1o00  5542  fsnd  5550  fv3  5584  dff2  5709  dff3im  5710  dffo4  5713  ffnfv  5723  ffvresb  5728  fsn2  5739  fconstfvm  5783  fnfvima  5800  fcof1o  5839  isocnv  5861  isotr  5866  riotaprop  5904  acexmidlemcase  5920  caovlem2d  6120  f1ocnvd  6129  caofcom  6170  resfunexgALT  6174  elxp7  6237  2ndrn  6250  1stconst  6288  2ndconst  6289  cnvf1olem  6291  poxp  6299  dftpos4  6330  dfsmo2  6354  tfrlem5  6381  tfrlemiex  6398  tfr1onlemsucaccv  6408  tfr1onlembfn  6411  tfr1onlemex  6414  tfr1onlemres  6416  tfrcllemsucaccv  6421  tfrcllembfn  6424  tfrcllemex  6427  tfrcllemres  6429  tfrcl  6431  frecabex  6465  frecabcl  6466  frecfcllem  6471  frecrdg  6475  oawordi  6536  nntri3  6564  nntr2  6570  nnmordi  6583  iserd  6627  relelec  6643  erth  6647  qliftfun  6685  mapsncnv  6763  mptelixpg  6802  bren  6815  pw2f1odclem  6904  findcard2d  6961  findcard2sd  6962  isinfinf  6967  tridc  6969  nnwetri  6986  undifdcss  6993  fiintim  7001  fisseneq  7004  fidcenumlemim  7027  sbthlemi9  7040  supisolem  7083  ordiso2  7110  updjud  7157  difinfsn  7175  ctssdccl  7186  nnnninfeq  7203  omniwomnimkv  7242  acfun  7290  exmidontriimlem2  7305  onntri45  7324  dftap2  7334  netap  7337  2omotaplemap  7340  ccfunen  7347  cc4f  7352  cc4n  7354  elni2  7398  dfplpq2  7438  dfmpq2  7439  enqbreq2  7441  enqdc1  7446  addcmpblnq  7451  addclnq  7459  nqpi  7462  addassnqg  7466  mulassnqg  7468  mulcanenq  7469  distrnqg  7471  1qec  7472  recexnq  7474  subhalfnqq  7498  enq0tr  7518  nqnq0pi  7522  nq0nn  7526  mulcanenq0ec  7529  nnnq0lem1  7530  addclnq0  7535  distrnq0  7543  addassnq0lemcl  7545  elnp1st2nd  7560  prarloc  7587  addlocprlemlt  7615  addlocprlemeq  7617  addlocprlemgt  7618  addclpr  7621  nqprm  7626  mullocprlem  7654  mullocpr  7655  mulclpr  7656  ltpopr  7679  ltaddpr  7681  ltexprlemm  7684  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemrnd  7689  ltexprlemdisj  7690  addcanprleml  7698  addcanprlemu  7699  addcanprg  7700  recexprlemm  7708  recexprlemopl  7709  recexprlemopu  7711  recexprlemrnd  7713  recexprlemdisj  7714  cauappcvgprlemm  7729  cauappcvgprlemopl  7730  cauappcvgprlemopu  7732  cauappcvgprlemrnd  7734  cauappcvgprlemdisj  7735  cauappcvgprlemlim  7745  caucvgprlemnkj  7750  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemopu  7755  caucvgprlemrnd  7757  caucvgprlemlim  7765  caucvgprprlemnkltj  7773  caucvgprprlemnkeqj  7774  caucvgprprlemnjltk  7775  caucvgprprlemm  7780  caucvgprprlemopl  7781  caucvgprprlemopu  7783  caucvgprprlemrnd  7785  caucvgprprlemexbt  7790  caucvgprprlemlim  7795  suplocexprlemrl  7801  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemex  7806  suplocexprlemub  7807  prsrlem1  7826  mulclsr  7838  mulasssrg  7842  distrsrg  7843  suplocsrlemb  7890  elreal2  7914  axmulass  7957  axdistr  7958  axcaucvglemcau  7982  add20  8518  mullt0  8524  rereim  8630  ltmul1  8636  cru  8646  mulap0r  8659  aprcl  8690  aptap  8694  divmuldivap  8756  divmuleqap  8761  divadddivap  8771  divmuldivapd  8876  divmuleqapd  8877  div2subap  8881  ltmul12a  8904  lemul12a  8906  lemulge11  8910  lediv12a  8938  lediv2a  8939  recgt1i  8942  recreclt  8944  ledivp1  8947  lemul1ad  8983  lemul2ad  8984  ltmul12ad  8985  lemul12ad  8986  lemul12bd  8987  nndivre  9043  nndivtr  9049  halfaddsubcl  9241  halfaddsub  9242  lt2halves  9244  nnrecl  9264  elnn0nn  9308  elnnnn0b  9310  elnnnn0c  9311  nn0addge1  9312  nn0addge2  9313  xnn0xrnemnf  9341  elnn0z  9356  elnnz1  9366  nzadd  9395  elz2  9414  zdivadd  9432  zdivmul  9433  zextle  9434  peano2uz2  9450  uzind  9454  btwnz  9462  uzss  9639  eluzp1m1  9642  infregelbex  9689  eluz2b2  9694  qre  9716  qaddcl  9726  qmulcl  9728  qreccl  9733  irradd  9737  irrmul  9738  elpqb  9741  cnref1o  9742  rprege0  9760  rprene0  9763  rpreap0  9764  rpcnne0  9765  rpcnap0  9766  rpregt0d  9795  rprege0d  9796  rprene0d  9797  rpcnne0d  9798  lediv2ad  9811  ledivge1le  9818  lediv12ad  9848  nnledivrp  9858  nn0ledivnn  9859  xrlttri3  9889  xrrebnd  9911  xrrege0  9917  xnn0xadd0  9959  xlesubadd  9975  elioo4g  10026  ioomax  10040  iccmax  10041  divelunit  10094  elfz5  10109  uzsubsubfz  10139  fzopth  10153  fzass4  10154  fzrev2  10177  uzsplit  10184  elfz2nn0  10204  difelfzle  10226  1fv  10231  4fvwrd4  10232  fzo1fzo0n0  10276  elfzom1elp1fzo  10295  subfzo0  10335  infssuzex  10340  qtri3or  10347  adddivflid  10399  flltdivnn0lt  10411  intfracq  10429  modqid2  10460  modfzo0difsn  10504  seq3val  10569  seqvalcd  10570  iseqf1olemqcl  10608  iseqf1olemnab  10610  iseqf1olemab  10611  iseqf1olemmo  10614  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seqf1oglem1  10628  seqf1oglem2  10629  expclzaplem  10672  leexp1a  10703  expubnd  10705  le2sq2  10724  sumsqeq0  10727  bernneq  10769  expnlbnd  10773  nn0opthd  10831  faclbnd6  10853  facavg  10855  seq3coll  10951  wrdnval  10982  shftlem  10998  shftfvalg  11000  shftfval  11003  cvg1nlemcau  11166  cvg1nlemres  11167  rexuz3  11172  resqrexlemcvg  11201  resqrexlemglsq  11204  resqrexlemga  11205  sqrtle  11218  sqrtlt  11219  sqrt11  11221  sqrtsq2  11225  absmul  11251  sqabs  11264  abslt  11270  absle  11271  lenegsq  11277  maxleastb  11396  maxltsup  11400  rexanre  11402  negfi  11410  xrmaxiflemab  11429  xrmaxiflemlub  11430  xrmaxltsup  11440  xrmaxadd  11443  climcn2  11491  mulcn2  11494  summodclem2a  11563  summodc  11565  fsum3  11569  fsum3cvg3  11578  fsumcl2lem  11580  fsumadd  11588  fsump1i  11615  fsum0diaglem  11622  mptfzshft  11624  fsumrev  11625  fsummulc2  11630  fsum00  11644  expcnvap0  11684  mertenslemi1  11717  ntrivcvgap0  11731  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  fprodrev  11801  fprodconst  11802  eftlub  11872  efieq  11917  sincos1sgn  11947  demoivreALT  11956  dvdsval3  11973  dvdscmul  12000  dvdsmulc  12001  dvdscmulr  12002  dvdsmulcr  12003  modmulconst  12005  dvds2ln  12006  ltoddhalfle  12075  nn0o  12089  divalg2  12108  ndvdssub  12112  ndvdsadd  12113  divgcdz  12163  gcd0id  12171  gcdaddm  12176  bezoutlemstep  12189  bezoutlemmain  12190  dfgcd3  12202  dfgcd2  12206  lcmcllem  12260  dvdslcm  12262  lcmgcdlem  12270  lcmgcdnn  12275  qredeq  12289  qredeu  12290  rpdvds  12292  divgcdcoprm0  12294  cncongr1  12296  cncongr2  12297  cncongrcoprm  12299  prmind2  12313  isprm5  12335  isprm6  12340  prmexpb  12344  cncongrprm  12350  sqrt2irrlem  12354  pw2dvdslemn  12358  oddpwdclemxy  12362  oddpwdclemdc  12366  oddpwdc  12367  hashdvds  12414  prmdiv  12428  hashgcdlem  12431  nnoddn2prmb  12456  pythagtriplem6  12464  pythagtriplem7  12465  pcpre1  12486  pccl  12493  pcmul  12495  pcdiv  12496  pcqmul  12497  pcqcl  12500  pcdvds  12509  pcndvds  12511  pcndvds2  12513  pc2dvds  12524  dvdsprmpweqle  12531  difsqpwdvds  12532  pcaddlem  12533  pcadd  12534  pcmptcl  12536  pcmpt  12537  fldivp1  12542  pcfac  12544  oddprmdvds  12548  infpnlem2  12554  4sqlem5  12576  4sqlem6  12577  4sqlem4a  12585  4sqexercise1  12592  4sqexercise2  12593  4sqlem13m  12597  4sqlem15  12599  4sqlem16  12600  ennnfonelemfun  12659  ennnfonelemim  12666  ctinfomlemom  12669  ctinfom  12670  ctinf  12672  ctiunctlemfo  12681  omctfn  12685  fnpr2ob  13042  ismgmid2  13082  fngsum  13090  igsumvalx  13091  gsumfzval  13093  gsum0g  13098  gsumval2  13099  issgrpd  13114  ismndd  13139  prdsidlem  13149  imasmnd2  13154  mhmf1o  13172  subsubm  13185  dfgrp2  13229  isgrpid2  13242  isgrpinv  13256  grplrinv  13259  dfgrp3mlem  13300  dfgrp3m  13301  dfgrp3me  13302  prdsinvlem  13310  imasgrp2  13316  mhmmnd  13322  issubg2m  13395  issubgrpd2  13396  grpissubg  13400  subsubg  13403  subgintm  13404  isnsg3  13413  nmzsubg  13416  eqgval  13429  eqgen  13433  isghmd  13458  ghmrn  13463  ghmpreima  13472  ghmf1o  13481  conjghm  13482  conjnmzb  13486  ghmpropd  13489  rinvmod  13515  imasabl  13542  rnglz  13577  isrngd  13585  srgdilem  13601  srglmhm  13625  srgrmhm  13626  ringdilem  13644  isringd  13673  ringsrg  13679  ringinvnzdiv  13682  imasring  13696  dvdsrd  13726  unitgrp  13748  isrim0  13793  isrhm2d  13797  rhmf1o  13800  rhmco  13806  rhmopp  13808  issubrng2  13842  subsubrng  13846  subrgugrp  13872  issubrg2  13873  subsubrg  13877  resrhm  13880  aprap  13918  lmodfopnelem2  13957  lsssubg  14009  islss3  14011  islss4  14014  lspsnel6  14040  lidlacl  14116  lidlsubg  14118  lidlrsppropdg  14127  2idlelbas  14148  cnfld1  14204  cnsubglem  14211  mulgghm2  14240  zndvds  14281  topgele  14349  tgcl  14384  epttop  14410  opnssneib  14476  iscnp4  14538  cnco  14541  cncnp  14550  cnrest2  14556  lmss  14566  txcnp  14591  txcn  14595  cnmpt12  14607  cnmpt22  14614  hmeof1o  14629  psmetres2  14653  distspace  14655  ismeti  14666  isxmetd  14667  xmetpsmet  14689  xblss2ps  14724  xblss2  14725  blcntrps  14735  blcntr  14736  blin2  14752  mopni3  14804  metequiv2  14816  bdmet  14822  xmettx  14830  cnbl0  14854  cnblcld  14855  tgioo  14874  elcncf1di  14899  dedekindeulemlu  14941  suplociccex  14945  dedekindicclemlu  14950  dedekindicc  14953  ivthinclemlopn  14956  ivthdec  14964  ivthreinc  14965  ivthdichlem  14971  cnplimcim  14987  limccnp2lem  14996  dvfvalap  15001  plymullem  15070  reeff1olem  15091  sin0pilem1  15101  pilem3  15103  ptolemy  15144  sincosq1sgn  15146  sinq12gt0  15150  ioocosf1o  15174  rprelogbmulexp  15276  perfectlem2  15320  lgslem3  15327  lgsne0  15363  gausslemma2dlem0b  15375  gausslemma2dlem0c  15376  lgsquadlem2  15403  lgsquad2lem2  15407  2lgsoddprmlem2  15431  2sqlem8  15448  bj-nnan  15466  bj-charfun  15537  bdop  15605  bdunexb  15650  bj-om  15667  findset  15675  bj-peano4  15685  bj-inf2vn  15704  bj-inf2vn2  15705  pwle2  15729  pwf1oexmid  15730  sbthom  15757  qdencn  15758  trilpolemlt1  15772