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  1481  nfand  1568  19.40  1631  equsexd  1729  sbcof2  1810  sbequ8  1847  eu2  2070  eu3h  2071  eu5  2073  mooran2  2099  datisi  2136  felapton  2140  darapti  2141  dimatis  2143  fresison  2144  fesapo  2146  reximssdv  2581  r19.26  2603  r19.29af2  2617  r19.40  2631  eqvinc  2861  eqvincg  2862  elrabd  2896  reu6  2927  reu3  2928  indifdir  3392  undif3ss  3397  un00  3470  eqifdc  3570  disjpr2  3657  prel12  3772  prneimg  3775  preqsn  3776  disjiun  3999  opth  4238  0nelop  4249  euotd  4255  opelopabsb  4261  ispod  4305  elon2  4377  unexb  4443  opeluu  4451  eusvnfb  4455  suc11g  4557  nlimsucg  4566  tfi  4582  vtoclr  4675  opthprc  4678  ideqg  4779  resiexg  4953  dminss  5044  imainss  5045  ssxpbm  5065  relrelss  5156  funopg  5251  fntpg  5273  fun11uni  5287  imain  5299  funimaexglem  5300  funssxp  5386  ffdm  5387  f00  5408  dffo2  5443  fodmrnu  5447  foco  5449  fun11iun  5483  f1o00  5497  fsnd  5505  fv3  5539  dff2  5661  dff3im  5662  dffo4  5665  ffnfv  5675  ffvresb  5680  fsn2  5691  fconstfvm  5735  fnfvima  5752  fcof1o  5790  isocnv  5812  isotr  5817  riotaprop  5854  acexmidlemcase  5870  caovlem2d  6067  f1ocnvd  6073  caofcom  6106  resfunexgALT  6109  elxp7  6171  2ndrn  6184  1stconst  6222  2ndconst  6223  cnvf1olem  6225  poxp  6233  dftpos4  6264  dfsmo2  6288  tfrlem5  6315  tfrlemiex  6332  tfr1onlemsucaccv  6342  tfr1onlembfn  6345  tfr1onlemex  6348  tfr1onlemres  6350  tfrcllemsucaccv  6355  tfrcllembfn  6358  tfrcllemex  6361  tfrcllemres  6363  tfrcl  6365  frecabex  6399  frecabcl  6400  frecfcllem  6405  frecrdg  6409  oawordi  6470  nntri3  6498  nntr2  6504  nnmordi  6517  iserd  6561  relelec  6575  erth  6579  qliftfun  6617  mapsncnv  6695  mptelixpg  6734  bren  6747  findcard2d  6891  findcard2sd  6892  isinfinf  6897  tridc  6899  nnwetri  6915  undifdcss  6922  fiintim  6928  fisseneq  6931  fidcenumlemim  6951  sbthlemi9  6964  supisolem  7007  ordiso2  7034  updjud  7081  difinfsn  7099  ctssdccl  7110  nnnninfeq  7126  omniwomnimkv  7165  acfun  7206  exmidontriimlem2  7221  onntri45  7240  dftap2  7250  netap  7253  2omotaplemap  7256  ccfunen  7263  cc4f  7268  cc4n  7270  elni2  7313  dfplpq2  7353  dfmpq2  7354  enqbreq2  7356  enqdc1  7361  addcmpblnq  7366  addclnq  7374  nqpi  7377  addassnqg  7381  mulassnqg  7383  mulcanenq  7384  distrnqg  7386  1qec  7387  recexnq  7389  subhalfnqq  7413  enq0tr  7433  nqnq0pi  7437  nq0nn  7441  mulcanenq0ec  7444  nnnq0lem1  7445  addclnq0  7450  distrnq0  7458  addassnq0lemcl  7460  elnp1st2nd  7475  prarloc  7502  addlocprlemlt  7530  addlocprlemeq  7532  addlocprlemgt  7533  addclpr  7536  nqprm  7541  mullocprlem  7569  mullocpr  7570  mulclpr  7571  ltpopr  7594  ltaddpr  7596  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemrnd  7604  ltexprlemdisj  7605  addcanprleml  7613  addcanprlemu  7614  addcanprg  7615  recexprlemm  7623  recexprlemopl  7624  recexprlemopu  7626  recexprlemrnd  7628  recexprlemdisj  7629  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemopu  7647  cauappcvgprlemrnd  7649  cauappcvgprlemdisj  7650  cauappcvgprlemlim  7660  caucvgprlemnkj  7665  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemopu  7670  caucvgprlemrnd  7672  caucvgprlemlim  7680  caucvgprprlemnkltj  7688  caucvgprprlemnkeqj  7689  caucvgprprlemnjltk  7690  caucvgprprlemm  7695  caucvgprprlemopl  7696  caucvgprprlemopu  7698  caucvgprprlemrnd  7700  caucvgprprlemexbt  7705  caucvgprprlemlim  7710  suplocexprlemrl  7716  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemex  7721  suplocexprlemub  7722  prsrlem1  7741  mulclsr  7753  mulasssrg  7757  distrsrg  7758  suplocsrlemb  7805  elreal2  7829  axmulass  7872  axdistr  7873  axcaucvglemcau  7897  add20  8431  mullt0  8437  rereim  8543  ltmul1  8549  cru  8559  mulap0r  8572  aprcl  8603  aptap  8607  divmuldivap  8669  divmuleqap  8674  divadddivap  8684  divmuldivapd  8789  divmuleqapd  8790  div2subap  8794  ltmul12a  8817  lemul12a  8819  lemulge11  8823  lediv12a  8851  lediv2a  8852  recgt1i  8855  recreclt  8857  ledivp1  8860  lemul1ad  8896  lemul2ad  8897  ltmul12ad  8898  lemul12ad  8899  lemul12bd  8900  nndivre  8955  nndivtr  8961  halfaddsubcl  9152  halfaddsub  9153  lt2halves  9154  nnrecl  9174  elnn0nn  9218  elnnnn0b  9220  elnnnn0c  9221  nn0addge1  9222  nn0addge2  9223  xnn0xrnemnf  9251  elnn0z  9266  elnnz1  9276  nzadd  9305  elz2  9324  zdivadd  9342  zdivmul  9343  zextle  9344  peano2uz2  9360  uzind  9364  btwnz  9372  uzss  9548  eluzp1m1  9551  infregelbex  9598  eluz2b2  9603  qre  9625  qaddcl  9635  qmulcl  9637  qreccl  9642  irradd  9646  irrmul  9647  elpqb  9649  cnref1o  9650  rprege0  9668  rprene0  9671  rpreap0  9672  rpcnne0  9673  rpcnap0  9674  rpregt0d  9703  rprege0d  9704  rprene0d  9705  rpcnne0d  9706  lediv2ad  9719  ledivge1le  9726  lediv12ad  9756  nnledivrp  9766  nn0ledivnn  9767  xrlttri3  9797  xrrebnd  9819  xrrege0  9825  xnn0xadd0  9867  xlesubadd  9883  elioo4g  9934  ioomax  9948  iccmax  9949  divelunit  10002  elfz5  10017  uzsubsubfz  10047  fzopth  10061  fzass4  10062  fzrev2  10085  uzsplit  10092  elfz2nn0  10112  difelfzle  10134  1fv  10139  4fvwrd4  10140  fzo1fzo0n0  10183  elfzom1elp1fzo  10202  subfzo0  10242  qtri3or  10243  adddivflid  10292  flltdivnn0lt  10304  intfracq  10320  modqid2  10351  modfzo0difsn  10395  seq3val  10458  seqvalcd  10459  iseqf1olemqcl  10486  iseqf1olemnab  10488  iseqf1olemab  10489  iseqf1olemmo  10492  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  expclzaplem  10544  leexp1a  10575  expubnd  10577  le2sq2  10596  sumsqeq0  10599  bernneq  10641  expnlbnd  10645  nn0opthd  10702  faclbnd6  10724  facavg  10726  seq3coll  10822  shftlem  10825  shftfvalg  10827  shftfval  10830  cvg1nlemcau  10993  cvg1nlemres  10994  rexuz3  10999  resqrexlemcvg  11028  resqrexlemglsq  11031  resqrexlemga  11032  sqrtle  11045  sqrtlt  11046  sqrt11  11048  sqrtsq2  11052  absmul  11078  sqabs  11091  abslt  11097  absle  11098  lenegsq  11104  maxleastb  11223  maxltsup  11227  rexanre  11229  negfi  11236  xrmaxiflemab  11255  xrmaxiflemlub  11256  xrmaxltsup  11266  xrmaxadd  11269  climcn2  11317  mulcn2  11320  summodclem2a  11389  summodc  11391  fsum3  11395  fsum3cvg3  11404  fsumcl2lem  11406  fsumadd  11414  fsump1i  11441  fsum0diaglem  11448  mptfzshft  11450  fsumrev  11451  fsummulc2  11456  fsum00  11470  expcnvap0  11510  mertenslemi1  11543  ntrivcvgap0  11557  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  fprodrev  11627  fprodconst  11628  eftlub  11698  efieq  11743  sincos1sgn  11772  demoivreALT  11781  dvdsval3  11798  dvdscmul  11825  dvdsmulc  11826  dvdscmulr  11827  dvdsmulcr  11828  modmulconst  11830  dvds2ln  11831  ltoddhalfle  11898  nn0o  11912  divalg2  11931  ndvdssub  11935  ndvdsadd  11936  infssuzex  11950  divgcdz  11972  gcd0id  11980  gcdaddm  11985  bezoutlemstep  11998  bezoutlemmain  11999  dfgcd3  12011  dfgcd2  12015  lcmcllem  12067  dvdslcm  12069  lcmgcdlem  12077  lcmgcdnn  12082  qredeq  12096  qredeu  12097  rpdvds  12099  divgcdcoprm0  12101  cncongr1  12103  cncongr2  12104  cncongrcoprm  12106  prmind2  12120  isprm5  12142  isprm6  12147  prmexpb  12151  cncongrprm  12157  sqrt2irrlem  12161  pw2dvdslemn  12165  oddpwdclemxy  12169  oddpwdclemdc  12173  oddpwdc  12174  hashdvds  12221  prmdiv  12235  hashgcdlem  12238  nnoddn2prmb  12262  pythagtriplem6  12270  pythagtriplem7  12271  pcpre1  12292  pccl  12299  pcmul  12301  pcdiv  12302  pcqmul  12303  pcqcl  12306  pcdvds  12314  pcndvds  12316  pcndvds2  12318  pc2dvds  12329  dvdsprmpweqle  12336  difsqpwdvds  12337  pcaddlem  12338  pcadd  12339  pcmptcl  12340  pcmpt  12341  fldivp1  12346  pcfac  12348  oddprmdvds  12352  infpnlem2  12358  4sqlem5  12380  4sqlem6  12381  4sqlem4a  12389  ennnfonelemfun  12418  ennnfonelemim  12425  ctinfomlemom  12428  ctinfom  12429  ctinf  12431  ctiunctlemfo  12440  omctfn  12444  fnpr2ob  12759  ismgmid2  12799  ismndd  12838  mhmf1o  12861  dfgrp2  12902  isgrpid2  12913  isgrpinv  12926  grplrinv  12927  dfgrp3mlem  12968  dfgrp3m  12969  dfgrp3me  12970  mhmmnd  12980  issubg2m  13049  issubgrpd2  13050  grpissubg  13054  subsubg  13057  subgintm  13058  isnsg3  13067  nmzsubg  13070  eqgval  13082  eqgen  13086  rinvmod  13112  srgdilem  13152  srglmhm  13176  srgrmhm  13177  ringdilem  13195  isringd  13220  ringsrg  13224  ringinvnzdiv  13227  dvdsrd  13263  unitgrp  13285  subrgugrp  13361  issubrg2  13362  subsubrg  13366  aprap  13376  lmodfopnelem2  13415  cnfld1  13469  cnsubglem  13476  topgele  13532  tgcl  13567  epttop  13593  opnssneib  13659  iscnp4  13721  cnco  13724  cncnp  13733  cnrest2  13739  lmss  13749  txcnp  13774  txcn  13778  cnmpt12  13790  cnmpt22  13797  hmeof1o  13812  psmetres2  13836  distspace  13838  ismeti  13849  isxmetd  13850  xmetpsmet  13872  xblss2ps  13907  xblss2  13908  blcntrps  13918  blcntr  13919  blin2  13935  mopni3  13987  metequiv2  13999  bdmet  14005  xmettx  14013  cnbl0  14037  cnblcld  14038  tgioo  14049  elcncf1di  14069  dedekindeulemlu  14102  suplociccex  14106  dedekindicclemlu  14111  dedekindicc  14114  ivthinclemlopn  14117  ivthdec  14125  cnplimcim  14139  limccnp2lem  14148  dvfvalap  14153  reeff1olem  14195  sin0pilem1  14205  pilem3  14207  ptolemy  14248  sincosq1sgn  14250  sinq12gt0  14254  ioocosf1o  14278  rprelogbmulexp  14377  lgslem3  14406  lgsne0  14442  2lgsoddprmlem2  14457  2sqlem8  14473  bj-nnan  14491  bj-charfun  14562  bdop  14630  bdunexb  14675  bj-om  14692  findset  14700  bj-peano4  14710  bj-inf2vn  14729  bj-inf2vn2  14730  pwle2  14751  pwf1oexmid  14752  sbthom  14777  qdencn  14778  trilpolemlt1  14792