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  607  biadanid  618  ioran  760  ordi  824  stdcndc  853  stdcndcOLD  854  dfandc  892  mpbi2and  952  mpbir2and  953  pm4.82  959  pm4.83dc  960  rnlem  985  ifp2  989  syl22anc  1275  syl112anc  1278  syl121anc  1279  syl211anc  1280  syl23anc  1281  syl32anc  1282  syl122anc  1283  syl212anc  1284  syl221anc  1285  syl222anc  1290  syl123anc  1291  syl132anc  1292  syl213anc  1293  syl231anc  1294  syl312anc  1295  syl321anc  1296  syl223anc  1300  syl232anc  1301  syl322anc  1302  syl233anc  1303  syl323anc  1304  syl332anc  1305  ecased  1386  19.26  1530  nfand  1617  19.40  1680  equsexd  1777  sbcof2  1858  sbequ8  1895  eu2  2124  eu3h  2125  eu5  2127  mooran2  2153  datisi  2190  felapton  2194  darapti  2195  dimatis  2197  fresison  2198  fesapo  2200  reximssdv  2637  r19.26  2660  r19.29af2  2674  r19.40  2688  eqvinc  2930  eqvincg  2931  elrabd  2965  reu6  2996  reu3  2997  indifdir  3465  undif3ss  3470  un00  3543  eqifdc  3646  disjpr2  3737  prel12  3859  prneimg  3862  preqsn  3863  disjiun  4088  opth  4335  0nelop  4346  euotd  4353  opelopabsb  4360  ispod  4407  elon2  4479  unexb  4545  opeluu  4553  eusvnfb  4557  suc11g  4661  nlimsucg  4670  tfi  4686  vtoclr  4780  opthprc  4783  ideqg  4887  resiexg  5064  dminss  5158  imainss  5159  ssxpbm  5179  relrelss  5270  funopg  5367  fununfun  5380  fntpg  5393  fun11uni  5407  imain  5419  funimaexglem  5420  funssxp  5512  ffdm  5513  f00  5537  dffo2  5572  fodmrnu  5576  foco  5579  fun11iun  5613  f1o00  5629  fsnd  5637  fv3  5671  dff2  5799  dff3im  5800  dffo4  5803  ffnfv  5813  ffvresb  5818  fsn2  5829  fconstfvm  5880  fnfvima  5899  resfvresima  5901  fcof1o  5940  isocnv  5962  isotr  5967  riotaprop  6007  acexmidlemcase  6023  caovlem2d  6225  f1ocnvd  6235  caofcom  6275  resfunexgALT  6279  elxp7  6342  2ndrn  6355  1stconst  6395  2ndconst  6396  cnvf1olem  6398  poxp  6406  ressuppss  6432  funsssuppss  6436  dftpos4  6472  dfsmo2  6496  tfrlem5  6523  tfrlemiex  6540  tfr1onlemsucaccv  6550  tfr1onlembfn  6553  tfr1onlemex  6556  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllembfn  6566  tfrcllemex  6569  tfrcllemres  6571  tfrcl  6573  frecabex  6607  frecabcl  6608  frecfcllem  6613  frecrdg  6617  oawordi  6680  nntri3  6708  nntr2  6714  nnmordi  6727  iserd  6771  relelec  6787  erth  6791  qliftfun  6829  mapsncnv  6907  mptelixpg  6946  bren  6960  pw2f1odclem  7063  findcard2d  7123  findcard2sd  7124  isinfinf  7129  tridc  7132  nnwetri  7151  undifdcss  7158  fiintim  7166  fisseneq  7170  fidcenumlemim  7194  sbthlemi9  7207  supisolem  7267  ordiso2  7294  updjud  7341  difinfsn  7359  ctssdccl  7370  nnnninfeq  7387  omniwomnimkv  7426  pr2cv  7462  acfun  7482  exmidontriimlem2  7497  onntri45  7519  dftap2  7530  netap  7533  2omotaplemap  7536  ccfunen  7543  cc4f  7548  cc4n  7550  elni2  7594  dfplpq2  7634  dfmpq2  7635  enqbreq2  7637  enqdc1  7642  addcmpblnq  7647  addclnq  7655  nqpi  7658  addassnqg  7662  mulassnqg  7664  mulcanenq  7665  distrnqg  7667  1qec  7668  recexnq  7670  subhalfnqq  7694  enq0tr  7714  nqnq0pi  7718  nq0nn  7722  mulcanenq0ec  7725  nnnq0lem1  7726  addclnq0  7731  distrnq0  7739  addassnq0lemcl  7741  elnp1st2nd  7756  prarloc  7783  addlocprlemlt  7811  addlocprlemeq  7813  addlocprlemgt  7814  addclpr  7817  nqprm  7822  mullocprlem  7850  mullocpr  7851  mulclpr  7852  ltpopr  7875  ltaddpr  7877  ltexprlemm  7880  ltexprlemopl  7881  ltexprlemopu  7883  ltexprlemrnd  7885  ltexprlemdisj  7886  addcanprleml  7894  addcanprlemu  7895  addcanprg  7896  recexprlemm  7904  recexprlemopl  7905  recexprlemopu  7907  recexprlemrnd  7909  recexprlemdisj  7910  cauappcvgprlemm  7925  cauappcvgprlemopl  7926  cauappcvgprlemopu  7928  cauappcvgprlemrnd  7930  cauappcvgprlemdisj  7931  cauappcvgprlemlim  7941  caucvgprlemnkj  7946  caucvgprlemm  7948  caucvgprlemopl  7949  caucvgprlemopu  7951  caucvgprlemrnd  7953  caucvgprlemlim  7961  caucvgprprlemnkltj  7969  caucvgprprlemnkeqj  7970  caucvgprprlemnjltk  7971  caucvgprprlemm  7976  caucvgprprlemopl  7977  caucvgprprlemopu  7979  caucvgprprlemrnd  7981  caucvgprprlemexbt  7986  caucvgprprlemlim  7991  suplocexprlemrl  7997  suplocexprlemru  7999  suplocexprlemdisj  8000  suplocexprlemloc  8001  suplocexprlemex  8002  suplocexprlemub  8003  prsrlem1  8022  mulclsr  8034  mulasssrg  8038  distrsrg  8039  suplocsrlemb  8086  elreal2  8110  axmulass  8153  axdistr  8154  axcaucvglemcau  8178  add20  8713  mullt0  8719  rereim  8825  ltmul1  8831  cru  8841  mulap0r  8854  aprcl  8885  aptap  8889  divmuldivap  8951  divmuleqap  8956  divadddivap  8966  divmuldivapd  9071  divmuleqapd  9072  div2subap  9076  ltmul12a  9099  lemul12a  9101  lemulge11  9105  lediv12a  9133  lediv2a  9134  recgt1i  9137  recreclt  9139  ledivp1  9142  lemul1ad  9178  lemul2ad  9179  ltmul12ad  9180  lemul12ad  9181  lemul12bd  9182  nndivre  9238  nndivtr  9244  halfaddsubcl  9436  halfaddsub  9437  lt2halves  9439  nnrecl  9459  elnn0nn  9503  elnnnn0b  9505  elnnnn0c  9506  nn0addge1  9507  nn0addge2  9508  xnn0xrnemnf  9538  elnn0z  9553  elnnz1  9563  nzadd  9593  elz2  9612  zdivadd  9630  zdivmul  9631  zextle  9632  peano2uz2  9648  uzind  9652  btwnz  9660  uzss  9838  eluzp1m1  9841  infregelbex  9893  eluz2b2  9898  qre  9920  qaddcl  9930  qmulcl  9932  qreccl  9937  irradd  9941  irrmul  9942  elpqb  9945  cnref1o  9946  rprege0  9964  rprene0  9967  rpreap0  9968  rpcnne0  9969  rpcnap0  9970  rpregt0d  9999  rprege0d  10000  rprene0d  10001  rpcnne0d  10002  lediv2ad  10015  ledivge1le  10022  lediv12ad  10052  nnledivrp  10062  nn0ledivnn  10063  xrlttri3  10093  xrrebnd  10115  xrrege0  10121  xnn0xadd0  10163  xlesubadd  10179  elioo4g  10230  ioomax  10244  iccmax  10245  divelunit  10298  elfz5  10314  uzsubsubfz  10344  fzopth  10358  fzass4  10359  fzrev2  10382  uzsplit  10389  elfz2nn0  10409  difelfzle  10431  1fv  10436  4fvwrd4  10437  fzo1fzo0n0  10485  elfzom1elp1fzo  10510  subfzo0  10551  infssuzex  10556  qtri3or  10563  adddivflid  10615  flltdivnn0lt  10627  intfracq  10645  modqid2  10676  modfzo0difsn  10720  seq3val  10785  seqvalcd  10786  iseqf1olemqcl  10824  iseqf1olemnab  10826  iseqf1olemab  10827  iseqf1olemmo  10830  seq3f1olemqsumkj  10836  seq3f1olemqsumk  10837  seqf1oglem1  10844  seqf1oglem2  10845  expclzaplem  10888  leexp1a  10919  expubnd  10921  le2sq2  10940  sumsqeq0  10943  bernneq  10985  expnlbnd  10989  nn0opthd  11047  faclbnd6  11069  facavg  11071  seq3coll  11169  hash2en  11170  wrdnval  11210  ccat0  11239  ccatsymb  11245  ccatalpha  11256  swrdspsleq  11314  pfxtrcfv  11340  pfxsuffeqwrdeq  11345  wrd2ind  11370  pfxccatin12lem2a  11374  pfxccatin12  11380  pfxccat3  11381  swrdccat  11382  pfxccatpfx1  11383  pfxccatpfx2  11384  swrdccatin1d  11390  swrdccatin2d  11391  shftlem  11456  shftfvalg  11458  shftfval  11461  cvg1nlemcau  11624  cvg1nlemres  11625  rexuz3  11630  resqrexlemcvg  11659  resqrexlemglsq  11662  resqrexlemga  11663  sqrtle  11676  sqrtlt  11677  sqrt11  11679  sqrtsq2  11683  absmul  11709  sqabs  11722  abslt  11728  absle  11729  lenegsq  11735  maxleastb  11854  maxltsup  11858  rexanre  11860  negfi  11868  xrmaxiflemab  11887  xrmaxiflemlub  11888  xrmaxltsup  11898  xrmaxadd  11901  climcn2  11949  mulcn2  11952  summodclem2a  12022  summodc  12024  fsum3  12028  fsum3cvg3  12037  fsumcl2lem  12039  fsumadd  12047  fsump1i  12074  fsum0diaglem  12081  mptfzshft  12083  fsumrev  12084  fsummulc2  12089  fsum00  12103  expcnvap0  12143  mertenslemi1  12176  ntrivcvgap0  12190  prodmodclem3  12216  prodmodclem2a  12217  zproddc  12220  fprodseq  12224  fprodrev  12260  fprodconst  12261  eftlub  12331  efieq  12376  sincos1sgn  12406  demoivreALT  12415  dvdsval3  12432  dvdscmul  12459  dvdsmulc  12460  dvdscmulr  12461  dvdsmulcr  12462  modmulconst  12464  dvds2ln  12465  ltoddhalfle  12534  nn0o  12548  divalg2  12567  ndvdssub  12571  ndvdsadd  12572  divgcdz  12622  gcd0id  12630  gcdaddm  12635  bezoutlemstep  12648  bezoutlemmain  12649  dfgcd3  12661  dfgcd2  12665  lcmcllem  12719  dvdslcm  12721  lcmgcdlem  12729  lcmgcdnn  12734  qredeq  12748  qredeu  12749  rpdvds  12751  divgcdcoprm0  12753  cncongr1  12755  cncongr2  12756  cncongrcoprm  12758  prmind2  12772  isprm5  12794  isprm6  12799  prmexpb  12803  cncongrprm  12809  sqrt2irrlem  12813  pw2dvdslemn  12817  oddpwdclemxy  12821  oddpwdclemdc  12825  oddpwdc  12826  hashdvds  12873  prmdiv  12887  hashgcdlem  12890  nnoddn2prmb  12915  pythagtriplem6  12923  pythagtriplem7  12924  pcpre1  12945  pccl  12952  pcmul  12954  pcdiv  12955  pcqmul  12956  pcqcl  12959  pcdvds  12968  pcndvds  12970  pcndvds2  12972  pc2dvds  12983  dvdsprmpweqle  12990  difsqpwdvds  12991  pcaddlem  12992  pcadd  12993  pcmptcl  12995  pcmpt  12996  fldivp1  13001  pcfac  13003  oddprmdvds  13007  infpnlem2  13013  4sqlem5  13035  4sqlem6  13036  4sqlem4a  13044  4sqexercise1  13051  4sqexercise2  13052  4sqlem13m  13056  4sqlem15  13058  4sqlem16  13059  ennnfonelemfun  13118  ennnfonelemim  13125  ctinfomlemom  13128  ctinfom  13129  ctinf  13131  ctiunctlemfo  13140  omctfn  13144  fnpr2ob  13503  ismgmid2  13543  fngsum  13551  igsumvalx  13552  gsumfzval  13554  gsum0g  13559  gsumval2  13560  issgrpd  13575  ismndd  13600  prdsidlem  13610  imasmnd2  13615  mhmf1o  13633  subsubm  13646  dfgrp2  13690  isgrpid2  13703  isgrpinv  13717  grplrinv  13720  dfgrp3mlem  13761  dfgrp3m  13762  dfgrp3me  13763  prdsinvlem  13771  imasgrp2  13777  mhmmnd  13783  issubg2m  13856  issubgrpd2  13857  grpissubg  13861  subsubg  13864  subgintm  13865  isnsg3  13874  nmzsubg  13877  eqgval  13890  eqgen  13894  isghmd  13919  ghmrn  13924  ghmpreima  13933  ghmf1o  13942  conjghm  13943  conjnmzb  13947  ghmpropd  13950  rinvmod  13976  imasabl  14003  rnglz  14039  isrngd  14047  srgdilem  14063  srglmhm  14087  srgrmhm  14088  ringdilem  14106  isringd  14135  ringsrg  14141  ringinvnzdiv  14144  imasring  14158  dvdsrd  14189  unitgrp  14211  isrim0  14256  isrhm2d  14260  rhmf1o  14263  rhmco  14269  rhmopp  14271  issubrng2  14305  subsubrng  14309  subrgugrp  14335  issubrg2  14336  subsubrg  14340  resrhm  14343  aprap  14382  lmodfopnelem2  14421  lsssubg  14473  islss3  14475  islss4  14478  lspsnel6  14504  lidlacl  14580  lidlsubg  14582  lidlrsppropdg  14591  2idlelbas  14612  cnfld1  14668  cnsubglem  14675  mulgghm2  14704  zndvds  14745  psrbagcon  14772  mplsubgfi  14802  topgele  14840  tgcl  14875  epttop  14901  opnssneib  14967  iscnp4  15029  cnco  15032  cncnp  15041  cnrest2  15047  lmss  15057  txcnp  15082  txcn  15086  cnmpt12  15098  cnmpt22  15105  hmeof1o  15120  psmetres2  15144  distspace  15146  ismeti  15157  isxmetd  15158  xmetpsmet  15180  xblss2ps  15215  xblss2  15216  blcntrps  15226  blcntr  15227  blin2  15243  mopni3  15295  metequiv2  15307  bdmet  15313  xmettx  15321  cnbl0  15345  cnblcld  15346  tgioo  15365  elcncf1di  15390  dedekindeulemlu  15432  suplociccex  15436  dedekindicclemlu  15441  dedekindicc  15444  ivthinclemlopn  15447  ivthdec  15455  ivthreinc  15456  ivthdichlem  15462  cnplimcim  15478  limccnp2lem  15487  dvfvalap  15492  plymullem  15561  reeff1olem  15582  sin0pilem1  15592  pilem3  15594  ptolemy  15635  sincosq1sgn  15637  sinq12gt0  15641  ioocosf1o  15665  rprelogbmulexp  15767  pellexlem3  15793  perfectlem2  15814  lgslem3  15821  lgsne0  15857  gausslemma2dlem0b  15869  gausslemma2dlem0c  15870  lgsquadlem2  15897  lgsquad2lem2  15901  2lgsoddprmlem2  15925  2sqlem8  15942  gropd  15988  grstructd2dom  15989  incistruhgr  16031  umgrislfupgrenlem  16071  umgrislfupgrdom  16072  uspgrupgrushgr  16123  usgrumgruspgr  16126  usgruspgrben  16127  usgrislfuspgrdom  16131  umgrvad2edg  16152  umgr2edgneu  16153  ushgredgedg  16167  ushgredgedgloop  16169  subgrprop3  16203  iswlkg  16270  wlk2f  16292  upgriswlkdc  16301  wlkv0  16310  wlklenvclwlk  16314  wlkepvtx  16316  upgr2wlkdc  16318  wlkres  16320  clwwlkccatlem  16341  clwwlkccat  16342  clwwlknbp  16356  clwwlknp  16358  clwwlkext2edg  16363  clwwlknon  16370  clwwlknonccat  16374  clwwlknonex2  16380  clwwlknonex2e  16381  trlsegvdeglem1  16401  bj-nnan  16454  bj-charfun  16523  bdop  16591  bdunexb  16636  bj-om  16653  findset  16661  bj-peano4  16671  bj-inf2vn  16690  bj-inf2vn2  16691  pwle2  16720  pwf1oexmid  16721  nnnninfex  16748  sbthom  16754  qdencn  16755  trilpolemlt1  16773  gfsumval  16809  gfsump1  16815