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  759  ordi  823  stdcndc  852  stdcndcOLD  853  dfandc  891  mpbi2and  951  mpbir2and  952  pm4.82  958  pm4.83dc  959  rnlem  984  ifp2  988  syl22anc  1274  syl112anc  1277  syl121anc  1278  syl211anc  1279  syl23anc  1280  syl32anc  1281  syl122anc  1282  syl212anc  1283  syl221anc  1284  syl222anc  1289  syl123anc  1290  syl132anc  1291  syl213anc  1292  syl231anc  1293  syl312anc  1294  syl321anc  1295  syl223anc  1299  syl232anc  1300  syl322anc  1301  syl233anc  1302  syl323anc  1303  syl332anc  1304  ecased  1385  19.26  1529  nfand  1616  19.40  1679  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  2636  r19.26  2659  r19.29af2  2673  r19.40  2687  eqvinc  2929  eqvincg  2930  elrabd  2964  reu6  2995  reu3  2996  indifdir  3463  undif3ss  3468  un00  3541  eqifdc  3642  disjpr2  3733  prel12  3854  prneimg  3857  preqsn  3858  disjiun  4083  opth  4329  0nelop  4340  euotd  4347  opelopabsb  4354  ispod  4401  elon2  4473  unexb  4539  opeluu  4547  eusvnfb  4551  suc11g  4655  nlimsucg  4664  tfi  4680  vtoclr  4774  opthprc  4777  ideqg  4881  resiexg  5058  dminss  5151  imainss  5152  ssxpbm  5172  relrelss  5263  funopg  5360  fununfun  5373  fntpg  5386  fun11uni  5400  imain  5412  funimaexglem  5413  funssxp  5504  ffdm  5505  f00  5528  dffo2  5563  fodmrnu  5567  foco  5570  fun11iun  5604  f1o00  5620  fsnd  5628  fv3  5662  dff2  5791  dff3im  5792  dffo4  5795  ffnfv  5805  ffvresb  5810  fsn2  5821  fconstfvm  5872  fnfvima  5889  resfvresima  5891  fcof1o  5930  isocnv  5952  isotr  5957  riotaprop  5997  acexmidlemcase  6013  caovlem2d  6215  f1ocnvd  6225  caofcom  6266  resfunexgALT  6270  elxp7  6333  2ndrn  6346  1stconst  6386  2ndconst  6387  cnvf1olem  6389  poxp  6397  dftpos4  6429  dfsmo2  6453  tfrlem5  6480  tfrlemiex  6497  tfr1onlemsucaccv  6507  tfr1onlembfn  6510  tfr1onlemex  6513  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllembfn  6523  tfrcllemex  6526  tfrcllemres  6528  tfrcl  6530  frecabex  6564  frecabcl  6565  frecfcllem  6570  frecrdg  6574  oawordi  6637  nntri3  6665  nntr2  6671  nnmordi  6684  iserd  6728  relelec  6744  erth  6748  qliftfun  6786  mapsncnv  6864  mptelixpg  6903  bren  6917  pw2f1odclem  7020  findcard2d  7080  findcard2sd  7081  isinfinf  7086  tridc  7089  nnwetri  7108  undifdcss  7115  fiintim  7123  fisseneq  7127  fidcenumlemim  7151  sbthlemi9  7164  supisolem  7207  ordiso2  7234  updjud  7281  difinfsn  7299  ctssdccl  7310  nnnninfeq  7327  omniwomnimkv  7366  pr2cv  7402  acfun  7422  exmidontriimlem2  7437  onntri45  7459  dftap2  7470  netap  7473  2omotaplemap  7476  ccfunen  7483  cc4f  7488  cc4n  7490  elni2  7534  dfplpq2  7574  dfmpq2  7575  enqbreq2  7577  enqdc1  7582  addcmpblnq  7587  addclnq  7595  nqpi  7598  addassnqg  7602  mulassnqg  7604  mulcanenq  7605  distrnqg  7607  1qec  7608  recexnq  7610  subhalfnqq  7634  enq0tr  7654  nqnq0pi  7658  nq0nn  7662  mulcanenq0ec  7665  nnnq0lem1  7666  addclnq0  7671  distrnq0  7679  addassnq0lemcl  7681  elnp1st2nd  7696  prarloc  7723  addlocprlemlt  7751  addlocprlemeq  7753  addlocprlemgt  7754  addclpr  7757  nqprm  7762  mullocprlem  7790  mullocpr  7791  mulclpr  7792  ltpopr  7815  ltaddpr  7817  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemrnd  7825  ltexprlemdisj  7826  addcanprleml  7834  addcanprlemu  7835  addcanprg  7836  recexprlemm  7844  recexprlemopl  7845  recexprlemopu  7847  recexprlemrnd  7849  recexprlemdisj  7850  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemopu  7868  cauappcvgprlemrnd  7870  cauappcvgprlemdisj  7871  cauappcvgprlemlim  7881  caucvgprlemnkj  7886  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemopu  7891  caucvgprlemrnd  7893  caucvgprlemlim  7901  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnjltk  7911  caucvgprprlemm  7916  caucvgprprlemopl  7917  caucvgprprlemopu  7919  caucvgprprlemrnd  7921  caucvgprprlemexbt  7926  caucvgprprlemlim  7931  suplocexprlemrl  7937  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemex  7942  suplocexprlemub  7943  prsrlem1  7962  mulclsr  7974  mulasssrg  7978  distrsrg  7979  suplocsrlemb  8026  elreal2  8050  axmulass  8093  axdistr  8094  axcaucvglemcau  8118  add20  8654  mullt0  8660  rereim  8766  ltmul1  8772  cru  8782  mulap0r  8795  aprcl  8826  aptap  8830  divmuldivap  8892  divmuleqap  8897  divadddivap  8907  divmuldivapd  9012  divmuleqapd  9013  div2subap  9017  ltmul12a  9040  lemul12a  9042  lemulge11  9046  lediv12a  9074  lediv2a  9075  recgt1i  9078  recreclt  9080  ledivp1  9083  lemul1ad  9119  lemul2ad  9120  ltmul12ad  9121  lemul12ad  9122  lemul12bd  9123  nndivre  9179  nndivtr  9185  halfaddsubcl  9377  halfaddsub  9378  lt2halves  9380  nnrecl  9400  elnn0nn  9444  elnnnn0b  9446  elnnnn0c  9447  nn0addge1  9448  nn0addge2  9449  xnn0xrnemnf  9477  elnn0z  9492  elnnz1  9502  nzadd  9532  elz2  9551  zdivadd  9569  zdivmul  9570  zextle  9571  peano2uz2  9587  uzind  9591  btwnz  9599  uzss  9777  eluzp1m1  9780  infregelbex  9832  eluz2b2  9837  qre  9859  qaddcl  9869  qmulcl  9871  qreccl  9876  irradd  9880  irrmul  9881  elpqb  9884  cnref1o  9885  rprege0  9903  rprene0  9906  rpreap0  9907  rpcnne0  9908  rpcnap0  9909  rpregt0d  9938  rprege0d  9939  rprene0d  9940  rpcnne0d  9941  lediv2ad  9954  ledivge1le  9961  lediv12ad  9991  nnledivrp  10001  nn0ledivnn  10002  xrlttri3  10032  xrrebnd  10054  xrrege0  10060  xnn0xadd0  10102  xlesubadd  10118  elioo4g  10169  ioomax  10183  iccmax  10184  divelunit  10237  elfz5  10252  uzsubsubfz  10282  fzopth  10296  fzass4  10297  fzrev2  10320  uzsplit  10327  elfz2nn0  10347  difelfzle  10369  1fv  10374  4fvwrd4  10375  fzo1fzo0n0  10423  elfzom1elp1fzo  10448  subfzo0  10489  infssuzex  10494  qtri3or  10501  adddivflid  10553  flltdivnn0lt  10565  intfracq  10583  modqid2  10614  modfzo0difsn  10658  seq3val  10723  seqvalcd  10724  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemmo  10768  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seqf1oglem1  10782  seqf1oglem2  10783  expclzaplem  10826  leexp1a  10857  expubnd  10859  le2sq2  10878  sumsqeq0  10881  bernneq  10923  expnlbnd  10927  nn0opthd  10985  faclbnd6  11007  facavg  11009  seq3coll  11107  hash2en  11108  wrdnval  11148  ccat0  11177  ccatsymb  11183  ccatalpha  11194  swrdspsleq  11252  pfxtrcfv  11278  pfxsuffeqwrdeq  11283  wrd2ind  11308  pfxccatin12lem2a  11312  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  pfxccatpfx1  11321  pfxccatpfx2  11322  swrdccatin1d  11328  swrdccatin2d  11329  shftlem  11394  shftfvalg  11396  shftfval  11399  cvg1nlemcau  11562  cvg1nlemres  11563  rexuz3  11568  resqrexlemcvg  11597  resqrexlemglsq  11600  resqrexlemga  11601  sqrtle  11614  sqrtlt  11615  sqrt11  11617  sqrtsq2  11621  absmul  11647  sqabs  11660  abslt  11666  absle  11667  lenegsq  11673  maxleastb  11792  maxltsup  11796  rexanre  11798  negfi  11806  xrmaxiflemab  11825  xrmaxiflemlub  11826  xrmaxltsup  11836  xrmaxadd  11839  climcn2  11887  mulcn2  11890  summodclem2a  11960  summodc  11962  fsum3  11966  fsum3cvg3  11975  fsumcl2lem  11977  fsumadd  11985  fsump1i  12012  fsum0diaglem  12019  mptfzshft  12021  fsumrev  12022  fsummulc2  12027  fsum00  12041  expcnvap0  12081  mertenslemi1  12114  ntrivcvgap0  12128  prodmodclem3  12154  prodmodclem2a  12155  zproddc  12158  fprodseq  12162  fprodrev  12198  fprodconst  12199  eftlub  12269  efieq  12314  sincos1sgn  12344  demoivreALT  12353  dvdsval3  12370  dvdscmul  12397  dvdsmulc  12398  dvdscmulr  12399  dvdsmulcr  12400  modmulconst  12402  dvds2ln  12403  ltoddhalfle  12472  nn0o  12486  divalg2  12505  ndvdssub  12509  ndvdsadd  12510  divgcdz  12560  gcd0id  12568  gcdaddm  12573  bezoutlemstep  12586  bezoutlemmain  12587  dfgcd3  12599  dfgcd2  12603  lcmcllem  12657  dvdslcm  12659  lcmgcdlem  12667  lcmgcdnn  12672  qredeq  12686  qredeu  12687  rpdvds  12689  divgcdcoprm0  12691  cncongr1  12693  cncongr2  12694  cncongrcoprm  12696  prmind2  12710  isprm5  12732  isprm6  12737  prmexpb  12741  cncongrprm  12747  sqrt2irrlem  12751  pw2dvdslemn  12755  oddpwdclemxy  12759  oddpwdclemdc  12763  oddpwdc  12764  hashdvds  12811  prmdiv  12825  hashgcdlem  12828  nnoddn2prmb  12853  pythagtriplem6  12861  pythagtriplem7  12862  pcpre1  12883  pccl  12890  pcmul  12892  pcdiv  12893  pcqmul  12894  pcqcl  12897  pcdvds  12906  pcndvds  12908  pcndvds2  12910  pc2dvds  12921  dvdsprmpweqle  12928  difsqpwdvds  12929  pcaddlem  12930  pcadd  12931  pcmptcl  12933  pcmpt  12934  fldivp1  12939  pcfac  12941  oddprmdvds  12945  infpnlem2  12951  4sqlem5  12973  4sqlem6  12974  4sqlem4a  12982  4sqexercise1  12989  4sqexercise2  12990  4sqlem13m  12994  4sqlem15  12996  4sqlem16  12997  ennnfonelemfun  13056  ennnfonelemim  13063  ctinfomlemom  13066  ctinfom  13067  ctinf  13069  ctiunctlemfo  13078  omctfn  13082  fnpr2ob  13441  ismgmid2  13481  fngsum  13489  igsumvalx  13490  gsumfzval  13492  gsum0g  13497  gsumval2  13498  issgrpd  13513  ismndd  13538  prdsidlem  13548  imasmnd2  13553  mhmf1o  13571  subsubm  13584  dfgrp2  13628  isgrpid2  13641  isgrpinv  13655  grplrinv  13658  dfgrp3mlem  13699  dfgrp3m  13700  dfgrp3me  13701  prdsinvlem  13709  imasgrp2  13715  mhmmnd  13721  issubg2m  13794  issubgrpd2  13795  grpissubg  13799  subsubg  13802  subgintm  13803  isnsg3  13812  nmzsubg  13815  eqgval  13828  eqgen  13832  isghmd  13857  ghmrn  13862  ghmpreima  13871  ghmf1o  13880  conjghm  13881  conjnmzb  13885  ghmpropd  13888  rinvmod  13914  imasabl  13941  rnglz  13977  isrngd  13985  srgdilem  14001  srglmhm  14025  srgrmhm  14026  ringdilem  14044  isringd  14073  ringsrg  14079  ringinvnzdiv  14082  imasring  14096  dvdsrd  14127  unitgrp  14149  isrim0  14194  isrhm2d  14198  rhmf1o  14201  rhmco  14207  rhmopp  14209  issubrng2  14243  subsubrng  14247  subrgugrp  14273  issubrg2  14274  subsubrg  14278  resrhm  14281  aprap  14319  lmodfopnelem2  14358  lsssubg  14410  islss3  14412  islss4  14415  lspsnel6  14441  lidlacl  14517  lidlsubg  14519  lidlrsppropdg  14528  2idlelbas  14549  cnfld1  14605  cnsubglem  14612  mulgghm2  14641  zndvds  14682  mplsubgfi  14734  topgele  14772  tgcl  14807  epttop  14833  opnssneib  14899  iscnp4  14961  cnco  14964  cncnp  14973  cnrest2  14979  lmss  14989  txcnp  15014  txcn  15018  cnmpt12  15030  cnmpt22  15037  hmeof1o  15052  psmetres2  15076  distspace  15078  ismeti  15089  isxmetd  15090  xmetpsmet  15112  xblss2ps  15147  xblss2  15148  blcntrps  15158  blcntr  15159  blin2  15175  mopni3  15227  metequiv2  15239  bdmet  15245  xmettx  15253  cnbl0  15277  cnblcld  15278  tgioo  15297  elcncf1di  15322  dedekindeulemlu  15364  suplociccex  15368  dedekindicclemlu  15373  dedekindicc  15376  ivthinclemlopn  15379  ivthdec  15387  ivthreinc  15388  ivthdichlem  15394  cnplimcim  15410  limccnp2lem  15419  dvfvalap  15424  plymullem  15493  reeff1olem  15514  sin0pilem1  15524  pilem3  15526  ptolemy  15567  sincosq1sgn  15569  sinq12gt0  15573  ioocosf1o  15597  rprelogbmulexp  15699  perfectlem2  15743  lgslem3  15750  lgsne0  15786  gausslemma2dlem0b  15798  gausslemma2dlem0c  15799  lgsquadlem2  15826  lgsquad2lem2  15830  2lgsoddprmlem2  15854  2sqlem8  15871  gropd  15917  grstructd2dom  15918  incistruhgr  15960  umgrislfupgrenlem  16000  umgrislfupgrdom  16001  uspgrupgrushgr  16052  usgrumgruspgr  16055  usgruspgrben  16056  usgrislfuspgrdom  16060  umgrvad2edg  16081  umgr2edgneu  16082  ushgredgedg  16096  ushgredgedgloop  16098  subgrprop3  16132  iswlkg  16199  wlk2f  16221  upgriswlkdc  16230  wlkv0  16239  wlklenvclwlk  16243  wlkepvtx  16245  upgr2wlkdc  16247  wlkres  16249  clwwlkccatlem  16270  clwwlkccat  16271  clwwlknbp  16285  clwwlknp  16287  clwwlkext2edg  16292  clwwlknon  16299  clwwlknonccat  16303  clwwlknonex2  16309  clwwlknonex2e  16310  trlsegvdeglem1  16330  bj-nnan  16383  bj-charfun  16453  bdop  16521  bdunexb  16566  bj-om  16583  findset  16591  bj-peano4  16601  bj-inf2vn  16620  bj-inf2vn2  16621  pwle2  16650  pwf1oexmid  16651  nnnninfex  16675  sbthom  16681  qdencn  16682  trilpolemlt1  16696  gfsumval  16732  gfsump1  16738