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  ioran  752  ordi  816  stdcndc  845  stdcndcOLD  846  dfandc  884  pm4.55dc  938  mpbi2and  943  mpbir2and  944  pm4.82  950  pm4.83dc  951  rnlem  976  syl22anc  1239  syl112anc  1242  syl121anc  1243  syl211anc  1244  syl23anc  1245  syl32anc  1246  syl122anc  1247  syl212anc  1248  syl221anc  1249  syl222anc  1254  syl123anc  1255  syl132anc  1256  syl213anc  1257  syl231anc  1258  syl312anc  1259  syl321anc  1260  syl223anc  1264  syl232anc  1265  syl322anc  1266  syl233anc  1267  syl323anc  1268  syl332anc  1269  ecased  1349  19.26  1479  nfand  1566  19.40  1629  equsexd  1727  sbcof2  1808  sbequ8  1845  eu2  2068  eu3h  2069  eu5  2071  mooran2  2097  datisi  2134  felapton  2138  darapti  2139  dimatis  2141  fresison  2142  fesapo  2144  reximssdv  2579  r19.26  2601  r19.29af2  2615  r19.40  2629  eqvinc  2858  eqvincg  2859  elrabd  2893  reu6  2924  reu3  2925  indifdir  3389  undif3ss  3394  un00  3467  eqifdc  3566  disjpr2  3653  prel12  3767  prneimg  3770  preqsn  3771  disjiun  3993  opth  4231  0nelop  4242  euotd  4248  opelopabsb  4254  ispod  4298  elon2  4370  unexb  4436  opeluu  4444  eusvnfb  4448  suc11g  4550  nlimsucg  4559  tfi  4575  vtoclr  4668  opthprc  4671  ideqg  4771  resiexg  4945  dminss  5035  imainss  5036  ssxpbm  5056  relrelss  5147  funopg  5242  fntpg  5264  fun11uni  5278  imain  5290  funimaexglem  5291  funssxp  5377  ffdm  5378  f00  5399  dffo2  5434  fodmrnu  5438  foco  5440  fun11iun  5474  f1o00  5488  fsnd  5496  fv3  5530  dff2  5652  dff3im  5653  dffo4  5656  ffnfv  5666  ffvresb  5671  fsn2  5682  fconstfvm  5726  fnfvima  5742  fcof1o  5780  isocnv  5802  isotr  5807  riotaprop  5844  acexmidlemcase  5860  caovlem2d  6057  f1ocnvd  6063  caofcom  6096  resfunexgALT  6099  elxp7  6161  2ndrn  6174  1stconst  6212  2ndconst  6213  cnvf1olem  6215  poxp  6223  dftpos4  6254  dfsmo2  6278  tfrlem5  6305  tfrlemiex  6322  tfr1onlemsucaccv  6332  tfr1onlembfn  6335  tfr1onlemex  6338  tfr1onlemres  6340  tfrcllemsucaccv  6345  tfrcllembfn  6348  tfrcllemex  6351  tfrcllemres  6353  tfrcl  6355  frecabex  6389  frecabcl  6390  frecfcllem  6395  frecrdg  6399  oawordi  6460  nntri3  6488  nntr2  6494  nnmordi  6507  iserd  6551  relelec  6565  erth  6569  qliftfun  6607  mapsncnv  6685  mptelixpg  6724  bren  6737  findcard2d  6881  findcard2sd  6882  isinfinf  6887  tridc  6889  nnwetri  6905  undifdcss  6912  fiintim  6918  fisseneq  6921  fidcenumlemim  6941  sbthlemi9  6954  supisolem  6997  ordiso2  7024  updjud  7071  difinfsn  7089  ctssdccl  7100  nnnninfeq  7116  omniwomnimkv  7155  acfun  7196  exmidontriimlem2  7211  onntri45  7230  ccfunen  7238  cc4f  7243  cc4n  7245  elni2  7288  dfplpq2  7328  dfmpq2  7329  enqbreq2  7331  enqdc1  7336  addcmpblnq  7341  addclnq  7349  nqpi  7352  addassnqg  7356  mulassnqg  7358  mulcanenq  7359  distrnqg  7361  1qec  7362  recexnq  7364  subhalfnqq  7388  enq0tr  7408  nqnq0pi  7412  nq0nn  7416  mulcanenq0ec  7419  nnnq0lem1  7420  addclnq0  7425  distrnq0  7433  addassnq0lemcl  7435  elnp1st2nd  7450  prarloc  7477  addlocprlemlt  7505  addlocprlemeq  7507  addlocprlemgt  7508  addclpr  7511  nqprm  7516  mullocprlem  7544  mullocpr  7545  mulclpr  7546  ltpopr  7569  ltaddpr  7571  ltexprlemm  7574  ltexprlemopl  7575  ltexprlemopu  7577  ltexprlemrnd  7579  ltexprlemdisj  7580  addcanprleml  7588  addcanprlemu  7589  addcanprg  7590  recexprlemm  7598  recexprlemopl  7599  recexprlemopu  7601  recexprlemrnd  7603  recexprlemdisj  7604  cauappcvgprlemm  7619  cauappcvgprlemopl  7620  cauappcvgprlemopu  7622  cauappcvgprlemrnd  7624  cauappcvgprlemdisj  7625  cauappcvgprlemlim  7635  caucvgprlemnkj  7640  caucvgprlemm  7642  caucvgprlemopl  7643  caucvgprlemopu  7645  caucvgprlemrnd  7647  caucvgprlemlim  7655  caucvgprprlemnkltj  7663  caucvgprprlemnkeqj  7664  caucvgprprlemnjltk  7665  caucvgprprlemm  7670  caucvgprprlemopl  7671  caucvgprprlemopu  7673  caucvgprprlemrnd  7675  caucvgprprlemexbt  7680  caucvgprprlemlim  7685  suplocexprlemrl  7691  suplocexprlemru  7693  suplocexprlemdisj  7694  suplocexprlemloc  7695  suplocexprlemex  7696  suplocexprlemub  7697  prsrlem1  7716  mulclsr  7728  mulasssrg  7732  distrsrg  7733  suplocsrlemb  7780  elreal2  7804  axmulass  7847  axdistr  7848  axcaucvglemcau  7872  add20  8405  mullt0  8411  rereim  8517  ltmul1  8523  cru  8533  mulap0r  8546  aprcl  8577  divmuldivap  8642  divmuleqap  8647  divadddivap  8657  divmuldivapd  8762  divmuleqapd  8763  div2subap  8767  ltmul12a  8790  lemul12a  8792  lemulge11  8796  lediv12a  8824  lediv2a  8825  recgt1i  8828  recreclt  8830  ledivp1  8833  lemul1ad  8869  lemul2ad  8870  ltmul12ad  8871  lemul12ad  8872  lemul12bd  8873  nndivre  8928  nndivtr  8934  halfaddsubcl  9125  halfaddsub  9126  lt2halves  9127  nnrecl  9147  elnn0nn  9191  elnnnn0b  9193  elnnnn0c  9194  nn0addge1  9195  nn0addge2  9196  xnn0xrnemnf  9224  elnn0z  9239  elnnz1  9249  nzadd  9278  elz2  9297  zdivadd  9315  zdivmul  9316  zextle  9317  peano2uz2  9333  uzind  9337  btwnz  9345  uzss  9521  eluzp1m1  9524  infregelbex  9571  eluz2b2  9576  qre  9598  qaddcl  9608  qmulcl  9610  qreccl  9615  irradd  9619  irrmul  9620  elpqb  9622  cnref1o  9623  rprege0  9639  rprene0  9642  rpreap0  9643  rpcnne0  9644  rpcnap0  9645  rpregt0d  9674  rprege0d  9675  rprene0d  9676  rpcnne0d  9677  lediv2ad  9690  ledivge1le  9697  lediv12ad  9727  nnledivrp  9737  nn0ledivnn  9738  xrlttri3  9768  xrrebnd  9790  xrrege0  9796  xnn0xadd0  9838  xlesubadd  9854  elioo4g  9905  ioomax  9919  iccmax  9920  divelunit  9973  elfz5  9987  uzsubsubfz  10017  fzopth  10031  fzass4  10032  fzrev2  10055  uzsplit  10062  elfz2nn0  10082  difelfzle  10104  1fv  10109  4fvwrd4  10110  fzo1fzo0n0  10153  elfzom1elp1fzo  10172  subfzo0  10212  qtri3or  10213  adddivflid  10262  flltdivnn0lt  10274  intfracq  10290  modqid2  10321  modfzo0difsn  10365  seq3val  10428  seqvalcd  10429  iseqf1olemqcl  10456  iseqf1olemnab  10458  iseqf1olemab  10459  iseqf1olemmo  10462  seq3f1olemqsumkj  10468  seq3f1olemqsumk  10469  expclzaplem  10514  leexp1a  10545  expubnd  10547  le2sq2  10565  sumsqeq0  10568  bernneq  10610  expnlbnd  10614  nn0opthd  10670  faclbnd6  10692  facavg  10694  seq3coll  10790  shftlem  10793  shftfvalg  10795  shftfval  10798  cvg1nlemcau  10961  cvg1nlemres  10962  rexuz3  10967  resqrexlemcvg  10996  resqrexlemglsq  10999  resqrexlemga  11000  sqrtle  11013  sqrtlt  11014  sqrt11  11016  sqrtsq2  11020  absmul  11046  sqabs  11059  abslt  11065  absle  11066  lenegsq  11072  maxleastb  11191  maxltsup  11195  rexanre  11197  negfi  11204  xrmaxiflemab  11223  xrmaxiflemlub  11224  xrmaxltsup  11234  xrmaxadd  11237  climcn2  11285  mulcn2  11288  summodclem2a  11357  summodc  11359  fsum3  11363  fsum3cvg3  11372  fsumcl2lem  11374  fsumadd  11382  fsump1i  11409  fsum0diaglem  11416  mptfzshft  11418  fsumrev  11419  fsummulc2  11424  fsum00  11438  expcnvap0  11478  mertenslemi1  11511  ntrivcvgap0  11525  prodmodclem3  11551  prodmodclem2a  11552  zproddc  11555  fprodseq  11559  fprodrev  11595  fprodconst  11596  eftlub  11666  efieq  11711  sincos1sgn  11740  demoivreALT  11749  dvdsval3  11766  dvdscmul  11793  dvdsmulc  11794  dvdscmulr  11795  dvdsmulcr  11796  modmulconst  11798  dvds2ln  11799  ltoddhalfle  11865  nn0o  11879  divalg2  11898  ndvdssub  11902  ndvdsadd  11903  infssuzex  11917  divgcdz  11939  gcd0id  11947  gcdaddm  11952  bezoutlemstep  11965  bezoutlemmain  11966  dfgcd3  11978  dfgcd2  11982  lcmcllem  12034  dvdslcm  12036  lcmgcdlem  12044  lcmgcdnn  12049  qredeq  12063  qredeu  12064  rpdvds  12066  divgcdcoprm0  12068  cncongr1  12070  cncongr2  12071  cncongrcoprm  12073  prmind2  12087  isprm5  12109  isprm6  12114  prmexpb  12118  cncongrprm  12124  sqrt2irrlem  12128  pw2dvdslemn  12132  oddpwdclemxy  12136  oddpwdclemdc  12140  oddpwdc  12141  hashdvds  12188  prmdiv  12202  hashgcdlem  12205  nnoddn2prmb  12229  pythagtriplem6  12237  pythagtriplem7  12238  pcpre1  12259  pccl  12266  pcmul  12268  pcdiv  12269  pcqmul  12270  pcqcl  12273  pcdvds  12281  pcndvds  12283  pcndvds2  12285  pc2dvds  12296  dvdsprmpweqle  12303  difsqpwdvds  12304  pcaddlem  12305  pcadd  12306  pcmptcl  12307  pcmpt  12308  fldivp1  12313  pcfac  12315  oddprmdvds  12319  infpnlem2  12325  4sqlem5  12347  4sqlem6  12348  4sqlem4a  12356  ennnfonelemfun  12385  ennnfonelemim  12392  ctinfomlemom  12395  ctinfom  12396  ctinf  12398  ctiunctlemfo  12407  omctfn  12411  ismgmid2  12674  ismndd  12713  mhmf1o  12733  dfgrp2  12773  isgrpid2  12784  isgrpinv  12797  grplrinv  12798  dfgrp3mlem  12838  dfgrp3m  12839  dfgrp3me  12840  mhmmnd  12850  rinvmod  12920  srgdilem  12958  srglmhm  12982  srgrmhm  12983  ringdilem  13001  isringd  13025  ringsrg  13029  ringinvnzdiv  13032  topgele  13107  tgcl  13144  epttop  13170  opnssneib  13236  iscnp4  13298  cnco  13301  cncnp  13310  cnrest2  13316  lmss  13326  txcnp  13351  txcn  13355  cnmpt12  13367  cnmpt22  13374  hmeof1o  13389  psmetres2  13413  distspace  13415  ismeti  13426  isxmetd  13427  xmetpsmet  13449  xblss2ps  13484  xblss2  13485  blcntrps  13495  blcntr  13496  blin2  13512  mopni3  13564  metequiv2  13576  bdmet  13582  xmettx  13590  cnbl0  13614  cnblcld  13615  tgioo  13626  elcncf1di  13646  dedekindeulemlu  13679  suplociccex  13683  dedekindicclemlu  13688  dedekindicc  13691  ivthinclemlopn  13694  ivthdec  13702  cnplimcim  13716  limccnp2lem  13725  dvfvalap  13730  reeff1olem  13772  sin0pilem1  13782  pilem3  13784  ptolemy  13825  sincosq1sgn  13827  sinq12gt0  13831  ioocosf1o  13855  rprelogbmulexp  13954  lgslem3  13983  lgsne0  14019  2sqlem8  14039  bj-nnan  14057  bj-charfun  14128  bdop  14196  bdunexb  14241  bj-om  14258  findset  14266  bj-peano4  14276  bj-inf2vn  14295  bj-inf2vn2  14296  pwle2  14317  pwf1oexmid  14318  sbthom  14344  qdencn  14345  trilpolemlt1  14359