Theorem jca 304

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 138	. 2 |- ( ps -> ( ch -> ( ps /\ ch ) ) )
4	1, 2, 3	sylc 62	1 |- ( ph -> ( ps /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  jca31  307  jca32  308  jcai  309  jctil  310  jctir  311  ancli  321  ancri  322  sylanbrc  415  jcab  598  ioran  747  ordi  811  stdcndc  840  stdcndcOLD  841  dfandc  879  pm4.55dc  933  mpbi2and  938  mpbir2and  939  pm4.82  945  pm4.83dc  946  rnlem  971  syl22anc  1234  syl112anc  1237  syl121anc  1238  syl211anc  1239  syl23anc  1240  syl32anc  1241  syl122anc  1242  syl212anc  1243  syl221anc  1244  syl222anc  1249  syl123anc  1250  syl132anc  1251  syl213anc  1252  syl231anc  1253  syl312anc  1254  syl321anc  1255  syl223anc  1259  syl232anc  1260  syl322anc  1261  syl233anc  1262  syl323anc  1263  syl332anc  1264  ecased  1344  19.26  1474  nfand  1561  19.40  1624  equsexd  1722  sbcof2  1803  sbequ8  1840  eu2  2063  eu3h  2064  eu5  2066  mooran2  2092  datisi  2129  felapton  2133  darapti  2134  dimatis  2136  fresison  2137  fesapo  2139  reximssdv  2574  r19.26  2596  r19.29af2  2610  r19.40  2624  eqvinc  2853  eqvincg  2854  elrabd  2888  reu6  2919  reu3  2920  indifdir  3383  undif3ss  3388  un00  3461  eqifdc  3560  disjpr2  3647  prel12  3758  prneimg  3761  preqsn  3762  disjiun  3984  opth  4222  0nelop  4233  euotd  4239  opelopabsb  4245  ispod  4289  elon2  4361  unexb  4427  opeluu  4435  eusvnfb  4439  suc11g  4541  nlimsucg  4550  tfi  4566  vtoclr  4659  opthprc  4662  ideqg  4762  resiexg  4936  dminss  5025  imainss  5026  ssxpbm  5046  relrelss  5137  funopg  5232  fntpg  5254  fun11uni  5268  imain  5280  funimaexglem  5281  funssxp  5367  ffdm  5368  f00  5389  dffo2  5424  fodmrnu  5428  foco  5430  fun11iun  5463  f1o00  5477  fsnd  5485  fv3  5519  dff2  5640  dff3im  5641  dffo4  5644  ffnfv  5654  ffvresb  5659  fsn2  5670  fconstfvm  5714  fnfvima  5730  fcof1o  5768  isocnv  5790  isotr  5795  riotaprop  5832  acexmidlemcase  5848  caovlem2d  6045  f1ocnvd  6051  caofcom  6084  resfunexgALT  6087  elxp7  6149  2ndrn  6162  1stconst  6200  2ndconst  6201  cnvf1olem  6203  poxp  6211  dftpos4  6242  dfsmo2  6266  tfrlem5  6293  tfrlemiex  6310  tfr1onlemsucaccv  6320  tfr1onlembfn  6323  tfr1onlemex  6326  tfr1onlemres  6328  tfrcllemsucaccv  6333  tfrcllembfn  6336  tfrcllemex  6339  tfrcllemres  6341  tfrcl  6343  frecabex  6377  frecabcl  6378  frecfcllem  6383  frecrdg  6387  oawordi  6448  nntri3  6476  nntr2  6482  nnmordi  6495  iserd  6539  relelec  6553  erth  6557  qliftfun  6595  mapsncnv  6673  mptelixpg  6712  bren  6725  findcard2d  6869  findcard2sd  6870  isinfinf  6875  tridc  6877  nnwetri  6893  undifdcss  6900  fiintim  6906  fisseneq  6909  fidcenumlemim  6929  sbthlemi9  6942  supisolem  6985  ordiso2  7012  updjud  7059  difinfsn  7077  ctssdccl  7088  nnnninfeq  7104  omniwomnimkv  7143  acfun  7184  exmidontriimlem2  7199  onntri45  7218  ccfunen  7226  cc4f  7231  cc4n  7233  elni2  7276  dfplpq2  7316  dfmpq2  7317  enqbreq2  7319  enqdc1  7324  addcmpblnq  7329  addclnq  7337  nqpi  7340  addassnqg  7344  mulassnqg  7346  mulcanenq  7347  distrnqg  7349  1qec  7350  recexnq  7352  subhalfnqq  7376  enq0tr  7396  nqnq0pi  7400  nq0nn  7404  mulcanenq0ec  7407  nnnq0lem1  7408  addclnq0  7413  distrnq0  7421  addassnq0lemcl  7423  elnp1st2nd  7438  prarloc  7465  addlocprlemlt  7493  addlocprlemeq  7495  addlocprlemgt  7496  addclpr  7499  nqprm  7504  mullocprlem  7532  mullocpr  7533  mulclpr  7534  ltpopr  7557  ltaddpr  7559  ltexprlemm  7562  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemrnd  7567  ltexprlemdisj  7568  addcanprleml  7576  addcanprlemu  7577  addcanprg  7578  recexprlemm  7586  recexprlemopl  7587  recexprlemopu  7589  recexprlemrnd  7591  recexprlemdisj  7592  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemopu  7610  cauappcvgprlemrnd  7612  cauappcvgprlemdisj  7613  cauappcvgprlemlim  7623  caucvgprlemnkj  7628  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemopu  7633  caucvgprlemrnd  7635  caucvgprlemlim  7643  caucvgprprlemnkltj  7651  caucvgprprlemnkeqj  7652  caucvgprprlemnjltk  7653  caucvgprprlemm  7658  caucvgprprlemopl  7659  caucvgprprlemopu  7661  caucvgprprlemrnd  7663  caucvgprprlemexbt  7668  caucvgprprlemlim  7673  suplocexprlemrl  7679  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemex  7684  suplocexprlemub  7685  prsrlem1  7704  mulclsr  7716  mulasssrg  7720  distrsrg  7721  suplocsrlemb  7768  elreal2  7792  axmulass  7835  axdistr  7836  axcaucvglemcau  7860  add20  8393  mullt0  8399  rereim  8505  ltmul1  8511  cru  8521  mulap0r  8534  aprcl  8565  divmuldivap  8629  divmuleqap  8634  divadddivap  8644  divmuldivapd  8749  divmuleqapd  8750  div2subap  8754  ltmul12a  8776  lemul12a  8778  lemulge11  8782  lediv12a  8810  lediv2a  8811  recgt1i  8814  recreclt  8816  ledivp1  8819  lemul1ad  8855  lemul2ad  8856  ltmul12ad  8857  lemul12ad  8858  lemul12bd  8859  nndivre  8914  nndivtr  8920  halfaddsubcl  9111  halfaddsub  9112  lt2halves  9113  nnrecl  9133  elnn0nn  9177  elnnnn0b  9179  elnnnn0c  9180  nn0addge1  9181  nn0addge2  9182  xnn0xrnemnf  9210  elnn0z  9225  elnnz1  9235  nzadd  9264  elz2  9283  zdivadd  9301  zdivmul  9302  zextle  9303  peano2uz2  9319  uzind  9323  btwnz  9331  uzss  9507  eluzp1m1  9510  infregelbex  9557  eluz2b2  9562  qre  9584  qaddcl  9594  qmulcl  9596  qreccl  9601  irradd  9605  irrmul  9606  elpqb  9608  cnref1o  9609  rprege0  9625  rprene0  9628  rpreap0  9629  rpcnne0  9630  rpcnap0  9631  rpregt0d  9660  rprege0d  9661  rprene0d  9662  rpcnne0d  9663  lediv2ad  9676  ledivge1le  9683  lediv12ad  9713  nnledivrp  9723  nn0ledivnn  9724  xrlttri3  9754  xrrebnd  9776  xrrege0  9782  xnn0xadd0  9824  xlesubadd  9840  elioo4g  9891  ioomax  9905  iccmax  9906  divelunit  9959  elfz5  9973  uzsubsubfz  10003  fzopth  10017  fzass4  10018  fzrev2  10041  uzsplit  10048  elfz2nn0  10068  difelfzle  10090  1fv  10095  4fvwrd4  10096  fzo1fzo0n0  10139  elfzom1elp1fzo  10158  subfzo0  10198  qtri3or  10199  adddivflid  10248  flltdivnn0lt  10260  intfracq  10276  modqid2  10307  modfzo0difsn  10351  seq3val  10414  seqvalcd  10415  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemab  10445  iseqf1olemmo  10448  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  expclzaplem  10500  leexp1a  10531  expubnd  10533  le2sq2  10551  sumsqeq0  10554  bernneq  10596  expnlbnd  10600  nn0opthd  10656  faclbnd6  10678  facavg  10680  seq3coll  10777  shftlem  10780  shftfvalg  10782  shftfval  10785  cvg1nlemcau  10948  cvg1nlemres  10949  rexuz3  10954  resqrexlemcvg  10983  resqrexlemglsq  10986  resqrexlemga  10987  sqrtle  11000  sqrtlt  11001  sqrt11  11003  sqrtsq2  11007  absmul  11033  sqabs  11046  abslt  11052  absle  11053  lenegsq  11059  maxleastb  11178  maxltsup  11182  rexanre  11184  negfi  11191  xrmaxiflemab  11210  xrmaxiflemlub  11211  xrmaxltsup  11221  xrmaxadd  11224  climcn2  11272  mulcn2  11275  summodclem2a  11344  summodc  11346  fsum3  11350  fsum3cvg3  11359  fsumcl2lem  11361  fsumadd  11369  fsump1i  11396  fsum0diaglem  11403  mptfzshft  11405  fsumrev  11406  fsummulc2  11411  fsum00  11425  expcnvap0  11465  mertenslemi1  11498  ntrivcvgap0  11512  prodmodclem3  11538  prodmodclem2a  11539  zproddc  11542  fprodseq  11546  fprodrev  11582  fprodconst  11583  eftlub  11653  efieq  11698  sincos1sgn  11727  demoivreALT  11736  dvdsval3  11753  dvdscmul  11780  dvdsmulc  11781  dvdscmulr  11782  dvdsmulcr  11783  modmulconst  11785  dvds2ln  11786  ltoddhalfle  11852  nn0o  11866  divalg2  11885  ndvdssub  11889  ndvdsadd  11890  infssuzex  11904  divgcdz  11926  gcd0id  11934  gcdaddm  11939  bezoutlemstep  11952  bezoutlemmain  11953  dfgcd3  11965  dfgcd2  11969  lcmcllem  12021  dvdslcm  12023  lcmgcdlem  12031  lcmgcdnn  12036  qredeq  12050  qredeu  12051  rpdvds  12053  divgcdcoprm0  12055  cncongr1  12057  cncongr2  12058  cncongrcoprm  12060  prmind2  12074  isprm5  12096  isprm6  12101  prmexpb  12105  cncongrprm  12111  sqrt2irrlem  12115  pw2dvdslemn  12119  oddpwdclemxy  12123  oddpwdclemdc  12127  oddpwdc  12128  hashdvds  12175  prmdiv  12189  hashgcdlem  12192  nnoddn2prmb  12216  pythagtriplem6  12224  pythagtriplem7  12225  pcpre1  12246  pccl  12253  pcmul  12255  pcdiv  12256  pcqmul  12257  pcqcl  12260  pcdvds  12268  pcndvds  12270  pcndvds2  12272  pc2dvds  12283  dvdsprmpweqle  12290  difsqpwdvds  12291  pcaddlem  12292  pcadd  12293  pcmptcl  12294  pcmpt  12295  fldivp1  12300  pcfac  12302  oddprmdvds  12306  infpnlem2  12312  4sqlem5  12334  4sqlem6  12335  4sqlem4a  12343  ennnfonelemfun  12372  ennnfonelemim  12379  ctinfomlemom  12382  ctinfom  12383  ctinf  12385  ctiunctlemfo  12394  omctfn  12398  ismgmid2  12634  ismndd  12673  mhmf1o  12693  dfgrp2  12732  isgrpid2  12743  isgrpinv  12756  grplrinv  12757  topgele  12821  tgcl  12858  epttop  12884  opnssneib  12950  iscnp4  13012  cnco  13015  cncnp  13024  cnrest2  13030  lmss  13040  txcnp  13065  txcn  13069  cnmpt12  13081  cnmpt22  13088  hmeof1o  13103  psmetres2  13127  distspace  13129  ismeti  13140  isxmetd  13141  xmetpsmet  13163  xblss2ps  13198  xblss2  13199  blcntrps  13209  blcntr  13210  blin2  13226  mopni3  13278  metequiv2  13290  bdmet  13296  xmettx  13304  cnbl0  13328  cnblcld  13329  tgioo  13340  elcncf1di  13360  dedekindeulemlu  13393  suplociccex  13397  dedekindicclemlu  13402  dedekindicc  13405  ivthinclemlopn  13408  ivthdec  13416  cnplimcim  13430  limccnp2lem  13439  dvfvalap  13444  reeff1olem  13486  sin0pilem1  13496  pilem3  13498  ptolemy  13539  sincosq1sgn  13541  sinq12gt0  13545  ioocosf1o  13569  rprelogbmulexp  13668  lgslem3  13697  lgsne0  13733  2sqlem8  13753  bj-nnan  13771  bj-charfun  13842  bdop  13910  bdunexb  13955  bj-om  13972  findset  13980  bj-peano4  13990  bj-inf2vn  14009  bj-inf2vn2  14010  pwle2  14031  pwf1oexmid  14032  sbthom  14058  qdencn  14059  trilpolemlt1  14073