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  3419  undif3ss  3424  un00  3497  eqifdc  3596  disjpr2  3686  prel12  3801  prneimg  3804  preqsn  3805  disjiun  4028  opth  4270  0nelop  4281  euotd  4287  opelopabsb  4294  ispod  4339  elon2  4411  unexb  4477  opeluu  4485  eusvnfb  4489  suc11g  4593  nlimsucg  4602  tfi  4618  vtoclr  4711  opthprc  4714  ideqg  4817  resiexg  4991  dminss  5084  imainss  5085  ssxpbm  5105  relrelss  5196  funopg  5292  fntpg  5314  fun11uni  5328  imain  5340  funimaexglem  5341  funssxp  5427  ffdm  5428  f00  5449  dffo2  5484  fodmrnu  5488  foco  5491  fun11iun  5525  f1o00  5539  fsnd  5547  fv3  5581  dff2  5706  dff3im  5707  dffo4  5710  ffnfv  5720  ffvresb  5725  fsn2  5736  fconstfvm  5780  fnfvima  5797  fcof1o  5836  isocnv  5858  isotr  5863  riotaprop  5901  acexmidlemcase  5917  caovlem2d  6116  f1ocnvd  6125  caofcom  6161  resfunexgALT  6165  elxp7  6228  2ndrn  6241  1stconst  6279  2ndconst  6280  cnvf1olem  6282  poxp  6290  dftpos4  6321  dfsmo2  6345  tfrlem5  6372  tfrlemiex  6389  tfr1onlemsucaccv  6399  tfr1onlembfn  6402  tfr1onlemex  6405  tfr1onlemres  6407  tfrcllemsucaccv  6412  tfrcllembfn  6415  tfrcllemex  6418  tfrcllemres  6420  tfrcl  6422  frecabex  6456  frecabcl  6457  frecfcllem  6462  frecrdg  6466  oawordi  6527  nntri3  6555  nntr2  6561  nnmordi  6574  iserd  6618  relelec  6634  erth  6638  qliftfun  6676  mapsncnv  6754  mptelixpg  6793  bren  6806  pw2f1odclem  6895  findcard2d  6952  findcard2sd  6953  isinfinf  6958  tridc  6960  nnwetri  6977  undifdcss  6984  fiintim  6992  fisseneq  6995  fidcenumlemim  7018  sbthlemi9  7031  supisolem  7074  ordiso2  7101  updjud  7148  difinfsn  7166  ctssdccl  7177  nnnninfeq  7194  omniwomnimkv  7233  acfun  7274  exmidontriimlem2  7289  onntri45  7308  dftap2  7318  netap  7321  2omotaplemap  7324  ccfunen  7331  cc4f  7336  cc4n  7338  elni2  7381  dfplpq2  7421  dfmpq2  7422  enqbreq2  7424  enqdc1  7429  addcmpblnq  7434  addclnq  7442  nqpi  7445  addassnqg  7449  mulassnqg  7451  mulcanenq  7452  distrnqg  7454  1qec  7455  recexnq  7457  subhalfnqq  7481  enq0tr  7501  nqnq0pi  7505  nq0nn  7509  mulcanenq0ec  7512  nnnq0lem1  7513  addclnq0  7518  distrnq0  7526  addassnq0lemcl  7528  elnp1st2nd  7543  prarloc  7570  addlocprlemlt  7598  addlocprlemeq  7600  addlocprlemgt  7601  addclpr  7604  nqprm  7609  mullocprlem  7637  mullocpr  7638  mulclpr  7639  ltpopr  7662  ltaddpr  7664  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemrnd  7672  ltexprlemdisj  7673  addcanprleml  7681  addcanprlemu  7682  addcanprg  7683  recexprlemm  7691  recexprlemopl  7692  recexprlemopu  7694  recexprlemrnd  7696  recexprlemdisj  7697  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemopu  7715  cauappcvgprlemrnd  7717  cauappcvgprlemdisj  7718  cauappcvgprlemlim  7728  caucvgprlemnkj  7733  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemopu  7738  caucvgprlemrnd  7740  caucvgprlemlim  7748  caucvgprprlemnkltj  7756  caucvgprprlemnkeqj  7757  caucvgprprlemnjltk  7758  caucvgprprlemm  7763  caucvgprprlemopl  7764  caucvgprprlemopu  7766  caucvgprprlemrnd  7768  caucvgprprlemexbt  7773  caucvgprprlemlim  7778  suplocexprlemrl  7784  suplocexprlemru  7786  suplocexprlemdisj  7787  suplocexprlemloc  7788  suplocexprlemex  7789  suplocexprlemub  7790  prsrlem1  7809  mulclsr  7821  mulasssrg  7825  distrsrg  7826  suplocsrlemb  7873  elreal2  7897  axmulass  7940  axdistr  7941  axcaucvglemcau  7965  add20  8501  mullt0  8507  rereim  8613  ltmul1  8619  cru  8629  mulap0r  8642  aprcl  8673  aptap  8677  divmuldivap  8739  divmuleqap  8744  divadddivap  8754  divmuldivapd  8859  divmuleqapd  8860  div2subap  8864  ltmul12a  8887  lemul12a  8889  lemulge11  8893  lediv12a  8921  lediv2a  8922  recgt1i  8925  recreclt  8927  ledivp1  8930  lemul1ad  8966  lemul2ad  8967  ltmul12ad  8968  lemul12ad  8969  lemul12bd  8970  nndivre  9026  nndivtr  9032  halfaddsubcl  9224  halfaddsub  9225  lt2halves  9227  nnrecl  9247  elnn0nn  9291  elnnnn0b  9293  elnnnn0c  9294  nn0addge1  9295  nn0addge2  9296  xnn0xrnemnf  9324  elnn0z  9339  elnnz1  9349  nzadd  9378  elz2  9397  zdivadd  9415  zdivmul  9416  zextle  9417  peano2uz2  9433  uzind  9437  btwnz  9445  uzss  9622  eluzp1m1  9625  infregelbex  9672  eluz2b2  9677  qre  9699  qaddcl  9709  qmulcl  9711  qreccl  9716  irradd  9720  irrmul  9721  elpqb  9724  cnref1o  9725  rprege0  9743  rprene0  9746  rpreap0  9747  rpcnne0  9748  rpcnap0  9749  rpregt0d  9778  rprege0d  9779  rprene0d  9780  rpcnne0d  9781  lediv2ad  9794  ledivge1le  9801  lediv12ad  9831  nnledivrp  9841  nn0ledivnn  9842  xrlttri3  9872  xrrebnd  9894  xrrege0  9900  xnn0xadd0  9942  xlesubadd  9958  elioo4g  10009  ioomax  10023  iccmax  10024  divelunit  10077  elfz5  10092  uzsubsubfz  10122  fzopth  10136  fzass4  10137  fzrev2  10160  uzsplit  10167  elfz2nn0  10187  difelfzle  10209  1fv  10214  4fvwrd4  10215  fzo1fzo0n0  10259  elfzom1elp1fzo  10278  subfzo0  10318  infssuzex  10323  qtri3or  10330  adddivflid  10382  flltdivnn0lt  10394  intfracq  10412  modqid2  10443  modfzo0difsn  10487  seq3val  10552  seqvalcd  10553  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemab  10594  iseqf1olemmo  10597  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seqf1oglem1  10611  seqf1oglem2  10612  expclzaplem  10655  leexp1a  10686  expubnd  10688  le2sq2  10707  sumsqeq0  10710  bernneq  10752  expnlbnd  10756  nn0opthd  10814  faclbnd6  10836  facavg  10838  seq3coll  10934  wrdnval  10965  shftlem  10981  shftfvalg  10983  shftfval  10986  cvg1nlemcau  11149  cvg1nlemres  11150  rexuz3  11155  resqrexlemcvg  11184  resqrexlemglsq  11187  resqrexlemga  11188  sqrtle  11201  sqrtlt  11202  sqrt11  11204  sqrtsq2  11208  absmul  11234  sqabs  11247  abslt  11253  absle  11254  lenegsq  11260  maxleastb  11379  maxltsup  11383  rexanre  11385  negfi  11393  xrmaxiflemab  11412  xrmaxiflemlub  11413  xrmaxltsup  11423  xrmaxadd  11426  climcn2  11474  mulcn2  11477  summodclem2a  11546  summodc  11548  fsum3  11552  fsum3cvg3  11561  fsumcl2lem  11563  fsumadd  11571  fsump1i  11598  fsum0diaglem  11605  mptfzshft  11607  fsumrev  11608  fsummulc2  11613  fsum00  11627  expcnvap0  11667  mertenslemi1  11700  ntrivcvgap0  11714  prodmodclem3  11740  prodmodclem2a  11741  zproddc  11744  fprodseq  11748  fprodrev  11784  fprodconst  11785  eftlub  11855  efieq  11900  sincos1sgn  11930  demoivreALT  11939  dvdsval3  11956  dvdscmul  11983  dvdsmulc  11984  dvdscmulr  11985  dvdsmulcr  11986  modmulconst  11988  dvds2ln  11989  ltoddhalfle  12058  nn0o  12072  divalg2  12091  ndvdssub  12095  ndvdsadd  12096  divgcdz  12138  gcd0id  12146  gcdaddm  12151  bezoutlemstep  12164  bezoutlemmain  12165  dfgcd3  12177  dfgcd2  12181  lcmcllem  12235  dvdslcm  12237  lcmgcdlem  12245  lcmgcdnn  12250  qredeq  12264  qredeu  12265  rpdvds  12267  divgcdcoprm0  12269  cncongr1  12271  cncongr2  12272  cncongrcoprm  12274  prmind2  12288  isprm5  12310  isprm6  12315  prmexpb  12319  cncongrprm  12325  sqrt2irrlem  12329  pw2dvdslemn  12333  oddpwdclemxy  12337  oddpwdclemdc  12341  oddpwdc  12342  hashdvds  12389  prmdiv  12403  hashgcdlem  12406  nnoddn2prmb  12431  pythagtriplem6  12439  pythagtriplem7  12440  pcpre1  12461  pccl  12468  pcmul  12470  pcdiv  12471  pcqmul  12472  pcqcl  12475  pcdvds  12484  pcndvds  12486  pcndvds2  12488  pc2dvds  12499  dvdsprmpweqle  12506  difsqpwdvds  12507  pcaddlem  12508  pcadd  12509  pcmptcl  12511  pcmpt  12512  fldivp1  12517  pcfac  12519  oddprmdvds  12523  infpnlem2  12529  4sqlem5  12551  4sqlem6  12552  4sqlem4a  12560  4sqexercise1  12567  4sqexercise2  12568  4sqlem13m  12572  4sqlem15  12574  4sqlem16  12575  ennnfonelemfun  12634  ennnfonelemim  12641  ctinfomlemom  12644  ctinfom  12645  ctinf  12647  ctiunctlemfo  12656  omctfn  12660  fnpr2ob  12983  ismgmid2  13023  fngsum  13031  igsumvalx  13032  gsumfzval  13034  gsum0g  13039  gsumval2  13040  issgrpd  13055  ismndd  13078  mhmf1o  13102  subsubm  13115  dfgrp2  13159  isgrpid2  13172  isgrpinv  13186  grplrinv  13189  dfgrp3mlem  13230  dfgrp3m  13231  dfgrp3me  13232  imasgrp2  13240  mhmmnd  13246  issubg2m  13319  issubgrpd2  13320  grpissubg  13324  subsubg  13327  subgintm  13328  isnsg3  13337  nmzsubg  13340  eqgval  13353  eqgen  13357  isghmd  13382  ghmrn  13387  ghmpreima  13396  ghmf1o  13405  conjghm  13406  conjnmzb  13410  ghmpropd  13413  rinvmod  13439  imasabl  13466  rnglz  13501  isrngd  13509  srgdilem  13525  srglmhm  13549  srgrmhm  13550  ringdilem  13568  isringd  13597  ringsrg  13603  ringinvnzdiv  13606  imasring  13620  dvdsrd  13650  unitgrp  13672  isrim0  13717  isrhm2d  13721  rhmf1o  13724  rhmco  13730  rhmopp  13732  issubrng2  13766  subsubrng  13770  subrgugrp  13796  issubrg2  13797  subsubrg  13801  resrhm  13804  aprap  13842  lmodfopnelem2  13881  lsssubg  13933  islss3  13935  islss4  13938  lspsnel6  13964  lidlacl  14040  lidlsubg  14042  lidlrsppropdg  14051  2idlelbas  14072  cnfld1  14128  cnsubglem  14135  mulgghm2  14164  zndvds  14205  topgele  14265  tgcl  14300  epttop  14326  opnssneib  14392  iscnp4  14454  cnco  14457  cncnp  14466  cnrest2  14472  lmss  14482  txcnp  14507  txcn  14511  cnmpt12  14523  cnmpt22  14530  hmeof1o  14545  psmetres2  14569  distspace  14571  ismeti  14582  isxmetd  14583  xmetpsmet  14605  xblss2ps  14640  xblss2  14641  blcntrps  14651  blcntr  14652  blin2  14668  mopni3  14720  metequiv2  14732  bdmet  14738  xmettx  14746  cnbl0  14770  cnblcld  14771  tgioo  14790  elcncf1di  14815  dedekindeulemlu  14857  suplociccex  14861  dedekindicclemlu  14866  dedekindicc  14869  ivthinclemlopn  14872  ivthdec  14880  ivthreinc  14881  ivthdichlem  14887  cnplimcim  14903  limccnp2lem  14912  dvfvalap  14917  plymullem  14986  reeff1olem  15007  sin0pilem1  15017  pilem3  15019  ptolemy  15060  sincosq1sgn  15062  sinq12gt0  15066  ioocosf1o  15090  rprelogbmulexp  15192  perfectlem2  15236  lgslem3  15243  lgsne0  15279  gausslemma2dlem0b  15291  gausslemma2dlem0c  15292  lgsquadlem2  15319  lgsquad2lem2  15323  2lgsoddprmlem2  15347  2sqlem8  15364  bj-nnan  15382  bj-charfun  15453  bdop  15521  bdunexb  15566  bj-om  15583  findset  15591  bj-peano4  15601  bj-inf2vn  15620  bj-inf2vn2  15621  pwle2  15643  pwf1oexmid  15644  sbthom  15670  qdencn  15671  trilpolemlt1  15685