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  1492  nfand  1579  19.40  1642  equsexd  1740  sbcof2  1821  sbequ8  1858  eu2  2082  eu3h  2083  eu5  2085  mooran2  2111  datisi  2148  felapton  2152  darapti  2153  dimatis  2155  fresison  2156  fesapo  2158  reximssdv  2594  r19.26  2616  r19.29af2  2630  r19.40  2644  eqvinc  2875  eqvincg  2876  elrabd  2910  reu6  2941  reu3  2942  indifdir  3406  undif3ss  3411  un00  3484  eqifdc  3584  disjpr2  3671  prel12  3786  prneimg  3789  preqsn  3790  disjiun  4013  opth  4255  0nelop  4266  euotd  4272  opelopabsb  4278  ispod  4322  elon2  4394  unexb  4460  opeluu  4468  eusvnfb  4472  suc11g  4574  nlimsucg  4583  tfi  4599  vtoclr  4692  opthprc  4695  ideqg  4796  resiexg  4970  dminss  5061  imainss  5062  ssxpbm  5082  relrelss  5173  funopg  5269  fntpg  5291  fun11uni  5305  imain  5317  funimaexglem  5318  funssxp  5404  ffdm  5405  f00  5426  dffo2  5461  fodmrnu  5465  foco  5467  fun11iun  5501  f1o00  5515  fsnd  5523  fv3  5557  dff2  5681  dff3im  5682  dffo4  5685  ffnfv  5695  ffvresb  5700  fsn2  5711  fconstfvm  5755  fnfvima  5772  fcof1o  5811  isocnv  5833  isotr  5838  riotaprop  5876  acexmidlemcase  5892  caovlem2d  6090  f1ocnvd  6097  caofcom  6131  resfunexgALT  6134  elxp7  6196  2ndrn  6209  1stconst  6247  2ndconst  6248  cnvf1olem  6250  poxp  6258  dftpos4  6289  dfsmo2  6313  tfrlem5  6340  tfrlemiex  6357  tfr1onlemsucaccv  6367  tfr1onlembfn  6370  tfr1onlemex  6373  tfr1onlemres  6375  tfrcllemsucaccv  6380  tfrcllembfn  6383  tfrcllemex  6386  tfrcllemres  6388  tfrcl  6390  frecabex  6424  frecabcl  6425  frecfcllem  6430  frecrdg  6434  oawordi  6495  nntri3  6523  nntr2  6529  nnmordi  6542  iserd  6586  relelec  6602  erth  6606  qliftfun  6644  mapsncnv  6722  mptelixpg  6761  bren  6774  pw2f1odclem  6863  findcard2d  6920  findcard2sd  6921  isinfinf  6926  tridc  6928  nnwetri  6945  undifdcss  6952  fiintim  6958  fisseneq  6961  fidcenumlemim  6982  sbthlemi9  6995  supisolem  7038  ordiso2  7065  updjud  7112  difinfsn  7130  ctssdccl  7141  nnnninfeq  7157  omniwomnimkv  7196  acfun  7237  exmidontriimlem2  7252  onntri45  7271  dftap2  7281  netap  7284  2omotaplemap  7287  ccfunen  7294  cc4f  7299  cc4n  7301  elni2  7344  dfplpq2  7384  dfmpq2  7385  enqbreq2  7387  enqdc1  7392  addcmpblnq  7397  addclnq  7405  nqpi  7408  addassnqg  7412  mulassnqg  7414  mulcanenq  7415  distrnqg  7417  1qec  7418  recexnq  7420  subhalfnqq  7444  enq0tr  7464  nqnq0pi  7468  nq0nn  7472  mulcanenq0ec  7475  nnnq0lem1  7476  addclnq0  7481  distrnq0  7489  addassnq0lemcl  7491  elnp1st2nd  7506  prarloc  7533  addlocprlemlt  7561  addlocprlemeq  7563  addlocprlemgt  7564  addclpr  7567  nqprm  7572  mullocprlem  7600  mullocpr  7601  mulclpr  7602  ltpopr  7625  ltaddpr  7627  ltexprlemm  7630  ltexprlemopl  7631  ltexprlemopu  7633  ltexprlemrnd  7635  ltexprlemdisj  7636  addcanprleml  7644  addcanprlemu  7645  addcanprg  7646  recexprlemm  7654  recexprlemopl  7655  recexprlemopu  7657  recexprlemrnd  7659  recexprlemdisj  7660  cauappcvgprlemm  7675  cauappcvgprlemopl  7676  cauappcvgprlemopu  7678  cauappcvgprlemrnd  7680  cauappcvgprlemdisj  7681  cauappcvgprlemlim  7691  caucvgprlemnkj  7696  caucvgprlemm  7698  caucvgprlemopl  7699  caucvgprlemopu  7701  caucvgprlemrnd  7703  caucvgprlemlim  7711  caucvgprprlemnkltj  7719  caucvgprprlemnkeqj  7720  caucvgprprlemnjltk  7721  caucvgprprlemm  7726  caucvgprprlemopl  7727  caucvgprprlemopu  7729  caucvgprprlemrnd  7731  caucvgprprlemexbt  7736  caucvgprprlemlim  7741  suplocexprlemrl  7747  suplocexprlemru  7749  suplocexprlemdisj  7750  suplocexprlemloc  7751  suplocexprlemex  7752  suplocexprlemub  7753  prsrlem1  7772  mulclsr  7784  mulasssrg  7788  distrsrg  7789  suplocsrlemb  7836  elreal2  7860  axmulass  7903  axdistr  7904  axcaucvglemcau  7928  add20  8462  mullt0  8468  rereim  8574  ltmul1  8580  cru  8590  mulap0r  8603  aprcl  8634  aptap  8638  divmuldivap  8700  divmuleqap  8705  divadddivap  8715  divmuldivapd  8820  divmuleqapd  8821  div2subap  8825  ltmul12a  8848  lemul12a  8850  lemulge11  8854  lediv12a  8882  lediv2a  8883  recgt1i  8886  recreclt  8888  ledivp1  8891  lemul1ad  8927  lemul2ad  8928  ltmul12ad  8929  lemul12ad  8930  lemul12bd  8931  nndivre  8986  nndivtr  8992  halfaddsubcl  9183  halfaddsub  9184  lt2halves  9185  nnrecl  9205  elnn0nn  9249  elnnnn0b  9251  elnnnn0c  9252  nn0addge1  9253  nn0addge2  9254  xnn0xrnemnf  9282  elnn0z  9297  elnnz1  9307  nzadd  9336  elz2  9355  zdivadd  9373  zdivmul  9374  zextle  9375  peano2uz2  9391  uzind  9395  btwnz  9403  uzss  9580  eluzp1m1  9583  infregelbex  9630  eluz2b2  9635  qre  9657  qaddcl  9667  qmulcl  9669  qreccl  9674  irradd  9678  irrmul  9679  elpqb  9681  cnref1o  9682  rprege0  9700  rprene0  9703  rpreap0  9704  rpcnne0  9705  rpcnap0  9706  rpregt0d  9735  rprege0d  9736  rprene0d  9737  rpcnne0d  9738  lediv2ad  9751  ledivge1le  9758  lediv12ad  9788  nnledivrp  9798  nn0ledivnn  9799  xrlttri3  9829  xrrebnd  9851  xrrege0  9857  xnn0xadd0  9899  xlesubadd  9915  elioo4g  9966  ioomax  9980  iccmax  9981  divelunit  10034  elfz5  10049  uzsubsubfz  10079  fzopth  10093  fzass4  10094  fzrev2  10117  uzsplit  10124  elfz2nn0  10144  difelfzle  10166  1fv  10171  4fvwrd4  10172  fzo1fzo0n0  10215  elfzom1elp1fzo  10234  subfzo0  10274  qtri3or  10275  adddivflid  10325  flltdivnn0lt  10337  intfracq  10353  modqid2  10384  modfzo0difsn  10428  seq3val  10491  seqvalcd  10492  iseqf1olemqcl  10519  iseqf1olemnab  10521  iseqf1olemab  10522  iseqf1olemmo  10525  seq3f1olemqsumkj  10531  seq3f1olemqsumk  10532  expclzaplem  10578  leexp1a  10609  expubnd  10611  le2sq2  10630  sumsqeq0  10633  bernneq  10675  expnlbnd  10679  nn0opthd  10737  faclbnd6  10759  facavg  10761  seq3coll  10857  shftlem  10860  shftfvalg  10862  shftfval  10865  cvg1nlemcau  11028  cvg1nlemres  11029  rexuz3  11034  resqrexlemcvg  11063  resqrexlemglsq  11066  resqrexlemga  11067  sqrtle  11080  sqrtlt  11081  sqrt11  11083  sqrtsq2  11087  absmul  11113  sqabs  11126  abslt  11132  absle  11133  lenegsq  11139  maxleastb  11258  maxltsup  11262  rexanre  11264  negfi  11271  xrmaxiflemab  11290  xrmaxiflemlub  11291  xrmaxltsup  11301  xrmaxadd  11304  climcn2  11352  mulcn2  11355  summodclem2a  11424  summodc  11426  fsum3  11430  fsum3cvg3  11439  fsumcl2lem  11441  fsumadd  11449  fsump1i  11476  fsum0diaglem  11483  mptfzshft  11485  fsumrev  11486  fsummulc2  11491  fsum00  11505  expcnvap0  11545  mertenslemi1  11578  ntrivcvgap0  11592  prodmodclem3  11618  prodmodclem2a  11619  zproddc  11622  fprodseq  11626  fprodrev  11662  fprodconst  11663  eftlub  11733  efieq  11778  sincos1sgn  11807  demoivreALT  11816  dvdsval3  11833  dvdscmul  11860  dvdsmulc  11861  dvdscmulr  11862  dvdsmulcr  11863  modmulconst  11865  dvds2ln  11866  ltoddhalfle  11933  nn0o  11947  divalg2  11966  ndvdssub  11970  ndvdsadd  11971  infssuzex  11985  divgcdz  12007  gcd0id  12015  gcdaddm  12020  bezoutlemstep  12033  bezoutlemmain  12034  dfgcd3  12046  dfgcd2  12050  lcmcllem  12102  dvdslcm  12104  lcmgcdlem  12112  lcmgcdnn  12117  qredeq  12131  qredeu  12132  rpdvds  12134  divgcdcoprm0  12136  cncongr1  12138  cncongr2  12139  cncongrcoprm  12141  prmind2  12155  isprm5  12177  isprm6  12182  prmexpb  12186  cncongrprm  12192  sqrt2irrlem  12196  pw2dvdslemn  12200  oddpwdclemxy  12204  oddpwdclemdc  12208  oddpwdc  12209  hashdvds  12256  prmdiv  12270  hashgcdlem  12273  nnoddn2prmb  12297  pythagtriplem6  12305  pythagtriplem7  12306  pcpre1  12327  pccl  12334  pcmul  12336  pcdiv  12337  pcqmul  12338  pcqcl  12341  pcdvds  12350  pcndvds  12352  pcndvds2  12354  pc2dvds  12365  dvdsprmpweqle  12372  difsqpwdvds  12373  pcaddlem  12374  pcadd  12375  pcmptcl  12377  pcmpt  12378  fldivp1  12383  pcfac  12385  oddprmdvds  12389  infpnlem2  12395  4sqlem5  12417  4sqlem6  12418  4sqlem4a  12426  4sqexercise1  12433  4sqexercise2  12434  4sqlem13m  12438  4sqlem15  12440  4sqlem16  12441  ennnfonelemfun  12471  ennnfonelemim  12478  ctinfomlemom  12481  ctinfom  12482  ctinf  12484  ctiunctlemfo  12493  omctfn  12497  fnpr2ob  12819  ismgmid2  12859  fngsum  12867  igsumvalx  12868  gsum0g  12874  gsumval2  12875  issgrpd  12890  ismndd  12913  mhmf1o  12937  subsubm  12950  dfgrp2  12986  isgrpid2  12999  isgrpinv  13013  grplrinv  13016  dfgrp3mlem  13057  dfgrp3m  13058  dfgrp3me  13059  imasgrp2  13067  mhmmnd  13073  issubg2m  13145  issubgrpd2  13146  grpissubg  13150  subsubg  13153  subgintm  13154  isnsg3  13163  nmzsubg  13166  eqgval  13179  eqgen  13183  isghmd  13208  ghmrn  13213  ghmpreima  13222  ghmf1o  13231  conjghm  13232  conjnmzb  13236  ghmpropd  13239  rinvmod  13265  imasabl  13290  rnglz  13316  isrngd  13324  srgdilem  13340  srglmhm  13364  srgrmhm  13365  ringdilem  13383  isringd  13412  ringsrg  13416  ringinvnzdiv  13419  imasring  13431  dvdsrd  13461  unitgrp  13483  isrim0  13528  isrhm2d  13532  rhmf1o  13535  rhmco  13541  rhmopp  13543  issubrng2  13574  subsubrng  13578  subrgugrp  13604  issubrg2  13605  subsubrg  13609  aprap  13619  lmodfopnelem2  13658  lsssubg  13710  islss3  13712  islss4  13715  lspsnel6  13741  lidlacl  13817  lidlsubg  13819  lidlrsppropdg  13828  2idlelbas  13848  cnfld1  13892  cnsubglem  13899  mulgghm2  13923  topgele  14006  tgcl  14041  epttop  14067  opnssneib  14133  iscnp4  14195  cnco  14198  cncnp  14207  cnrest2  14213  lmss  14223  txcnp  14248  txcn  14252  cnmpt12  14264  cnmpt22  14271  hmeof1o  14286  psmetres2  14310  distspace  14312  ismeti  14323  isxmetd  14324  xmetpsmet  14346  xblss2ps  14381  xblss2  14382  blcntrps  14392  blcntr  14393  blin2  14409  mopni3  14461  metequiv2  14473  bdmet  14479  xmettx  14487  cnbl0  14511  cnblcld  14512  tgioo  14523  elcncf1di  14543  dedekindeulemlu  14576  suplociccex  14580  dedekindicclemlu  14585  dedekindicc  14588  ivthinclemlopn  14591  ivthdec  14599  cnplimcim  14613  limccnp2lem  14622  dvfvalap  14627  reeff1olem  14669  sin0pilem1  14679  pilem3  14681  ptolemy  14722  sincosq1sgn  14724  sinq12gt0  14728  ioocosf1o  14752  rprelogbmulexp  14851  lgslem3  14881  lgsne0  14917  2lgsoddprmlem2  14932  2sqlem8  14948  bj-nnan  14966  bj-charfun  15037  bdop  15105  bdunexb  15150  bj-om  15167  findset  15175  bj-peano4  15185  bj-inf2vn  15204  bj-inf2vn2  15205  pwle2  15227  pwf1oexmid  15228  sbthom  15253  qdencn  15254  trilpolemlt1  15268