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  605  biadanid  616  ioran  757  ordi  821  stdcndc  850  stdcndcOLD  851  dfandc  889  mpbi2and  949  mpbir2and  950  pm4.82  956  pm4.83dc  957  rnlem  982  ifp2  986  syl22anc  1272  syl112anc  1275  syl121anc  1276  syl211anc  1277  syl23anc  1278  syl32anc  1279  syl122anc  1280  syl212anc  1281  syl221anc  1282  syl222anc  1287  syl123anc  1288  syl132anc  1289  syl213anc  1290  syl231anc  1291  syl312anc  1292  syl321anc  1293  syl223anc  1297  syl232anc  1298  syl322anc  1299  syl233anc  1300  syl323anc  1301  syl332anc  1302  ecased  1383  19.26  1527  nfand  1614  19.40  1677  equsexd  1775  sbcof2  1856  sbequ8  1893  eu2  2122  eu3h  2123  eu5  2125  mooran2  2151  datisi  2188  felapton  2192  darapti  2193  dimatis  2195  fresison  2196  fesapo  2198  reximssdv  2634  r19.26  2657  r19.29af2  2671  r19.40  2685  eqvinc  2926  eqvincg  2927  elrabd  2961  reu6  2992  reu3  2993  indifdir  3460  undif3ss  3465  un00  3538  eqifdc  3639  disjpr2  3730  prel12  3849  prneimg  3852  preqsn  3853  disjiun  4078  opth  4323  0nelop  4334  euotd  4341  opelopabsb  4348  ispod  4395  elon2  4467  unexb  4533  opeluu  4541  eusvnfb  4545  suc11g  4649  nlimsucg  4658  tfi  4674  vtoclr  4767  opthprc  4770  ideqg  4873  resiexg  5050  dminss  5143  imainss  5144  ssxpbm  5164  relrelss  5255  funopg  5352  fununfun  5364  fntpg  5377  fun11uni  5391  imain  5403  funimaexglem  5404  funssxp  5493  ffdm  5494  f00  5517  dffo2  5552  fodmrnu  5556  foco  5559  fun11iun  5593  f1o00  5608  fsnd  5616  fv3  5650  dff2  5779  dff3im  5780  dffo4  5783  ffnfv  5793  ffvresb  5798  fsn2  5809  fconstfvm  5857  fnfvima  5874  fcof1o  5913  isocnv  5935  isotr  5940  riotaprop  5980  acexmidlemcase  5996  caovlem2d  6198  f1ocnvd  6208  caofcom  6249  resfunexgALT  6253  elxp7  6316  2ndrn  6329  1stconst  6367  2ndconst  6368  cnvf1olem  6370  poxp  6378  dftpos4  6409  dfsmo2  6433  tfrlem5  6460  tfrlemiex  6477  tfr1onlemsucaccv  6487  tfr1onlembfn  6490  tfr1onlemex  6493  tfr1onlemres  6495  tfrcllemsucaccv  6500  tfrcllembfn  6503  tfrcllemex  6506  tfrcllemres  6508  tfrcl  6510  frecabex  6544  frecabcl  6545  frecfcllem  6550  frecrdg  6554  oawordi  6615  nntri3  6643  nntr2  6649  nnmordi  6662  iserd  6706  relelec  6722  erth  6726  qliftfun  6764  mapsncnv  6842  mptelixpg  6881  bren  6895  pw2f1odclem  6995  findcard2d  7053  findcard2sd  7054  isinfinf  7059  tridc  7061  nnwetri  7078  undifdcss  7085  fiintim  7093  fisseneq  7096  fidcenumlemim  7119  sbthlemi9  7132  supisolem  7175  ordiso2  7202  updjud  7249  difinfsn  7267  ctssdccl  7278  nnnninfeq  7295  omniwomnimkv  7334  pr2cv  7370  acfun  7389  exmidontriimlem2  7404  onntri45  7426  dftap2  7437  netap  7440  2omotaplemap  7443  ccfunen  7450  cc4f  7455  cc4n  7457  elni2  7501  dfplpq2  7541  dfmpq2  7542  enqbreq2  7544  enqdc1  7549  addcmpblnq  7554  addclnq  7562  nqpi  7565  addassnqg  7569  mulassnqg  7571  mulcanenq  7572  distrnqg  7574  1qec  7575  recexnq  7577  subhalfnqq  7601  enq0tr  7621  nqnq0pi  7625  nq0nn  7629  mulcanenq0ec  7632  nnnq0lem1  7633  addclnq0  7638  distrnq0  7646  addassnq0lemcl  7648  elnp1st2nd  7663  prarloc  7690  addlocprlemlt  7718  addlocprlemeq  7720  addlocprlemgt  7721  addclpr  7724  nqprm  7729  mullocprlem  7757  mullocpr  7758  mulclpr  7759  ltpopr  7782  ltaddpr  7784  ltexprlemm  7787  ltexprlemopl  7788  ltexprlemopu  7790  ltexprlemrnd  7792  ltexprlemdisj  7793  addcanprleml  7801  addcanprlemu  7802  addcanprg  7803  recexprlemm  7811  recexprlemopl  7812  recexprlemopu  7814  recexprlemrnd  7816  recexprlemdisj  7817  cauappcvgprlemm  7832  cauappcvgprlemopl  7833  cauappcvgprlemopu  7835  cauappcvgprlemrnd  7837  cauappcvgprlemdisj  7838  cauappcvgprlemlim  7848  caucvgprlemnkj  7853  caucvgprlemm  7855  caucvgprlemopl  7856  caucvgprlemopu  7858  caucvgprlemrnd  7860  caucvgprlemlim  7868  caucvgprprlemnkltj  7876  caucvgprprlemnkeqj  7877  caucvgprprlemnjltk  7878  caucvgprprlemm  7883  caucvgprprlemopl  7884  caucvgprprlemopu  7886  caucvgprprlemrnd  7888  caucvgprprlemexbt  7893  caucvgprprlemlim  7898  suplocexprlemrl  7904  suplocexprlemru  7906  suplocexprlemdisj  7907  suplocexprlemloc  7908  suplocexprlemex  7909  suplocexprlemub  7910  prsrlem1  7929  mulclsr  7941  mulasssrg  7945  distrsrg  7946  suplocsrlemb  7993  elreal2  8017  axmulass  8060  axdistr  8061  axcaucvglemcau  8085  add20  8621  mullt0  8627  rereim  8733  ltmul1  8739  cru  8749  mulap0r  8762  aprcl  8793  aptap  8797  divmuldivap  8859  divmuleqap  8864  divadddivap  8874  divmuldivapd  8979  divmuleqapd  8980  div2subap  8984  ltmul12a  9007  lemul12a  9009  lemulge11  9013  lediv12a  9041  lediv2a  9042  recgt1i  9045  recreclt  9047  ledivp1  9050  lemul1ad  9086  lemul2ad  9087  ltmul12ad  9088  lemul12ad  9089  lemul12bd  9090  nndivre  9146  nndivtr  9152  halfaddsubcl  9344  halfaddsub  9345  lt2halves  9347  nnrecl  9367  elnn0nn  9411  elnnnn0b  9413  elnnnn0c  9414  nn0addge1  9415  nn0addge2  9416  xnn0xrnemnf  9444  elnn0z  9459  elnnz1  9469  nzadd  9499  elz2  9518  zdivadd  9536  zdivmul  9537  zextle  9538  peano2uz2  9554  uzind  9558  btwnz  9566  uzss  9743  eluzp1m1  9746  infregelbex  9793  eluz2b2  9798  qre  9820  qaddcl  9830  qmulcl  9832  qreccl  9837  irradd  9841  irrmul  9842  elpqb  9845  cnref1o  9846  rprege0  9864  rprene0  9867  rpreap0  9868  rpcnne0  9869  rpcnap0  9870  rpregt0d  9899  rprege0d  9900  rprene0d  9901  rpcnne0d  9902  lediv2ad  9915  ledivge1le  9922  lediv12ad  9952  nnledivrp  9962  nn0ledivnn  9963  xrlttri3  9993  xrrebnd  10015  xrrege0  10021  xnn0xadd0  10063  xlesubadd  10079  elioo4g  10130  ioomax  10144  iccmax  10145  divelunit  10198  elfz5  10213  uzsubsubfz  10243  fzopth  10257  fzass4  10258  fzrev2  10281  uzsplit  10288  elfz2nn0  10308  difelfzle  10330  1fv  10335  4fvwrd4  10336  fzo1fzo0n0  10383  elfzom1elp1fzo  10408  subfzo0  10448  infssuzex  10453  qtri3or  10460  adddivflid  10512  flltdivnn0lt  10524  intfracq  10542  modqid2  10573  modfzo0difsn  10617  seq3val  10682  seqvalcd  10683  iseqf1olemqcl  10721  iseqf1olemnab  10723  iseqf1olemab  10724  iseqf1olemmo  10727  seq3f1olemqsumkj  10733  seq3f1olemqsumk  10734  seqf1oglem1  10741  seqf1oglem2  10742  expclzaplem  10785  leexp1a  10816  expubnd  10818  le2sq2  10837  sumsqeq0  10840  bernneq  10882  expnlbnd  10886  nn0opthd  10944  faclbnd6  10966  facavg  10968  seq3coll  11064  hash2en  11065  wrdnval  11102  ccat0  11131  ccatsymb  11137  swrdspsleq  11199  pfxtrcfv  11225  pfxsuffeqwrdeq  11230  wrd2ind  11255  pfxccatin12lem2a  11259  pfxccatin12  11265  pfxccat3  11266  swrdccat  11267  pfxccatpfx1  11268  pfxccatpfx2  11269  swrdccatin1d  11275  swrdccatin2d  11276  shftlem  11327  shftfvalg  11329  shftfval  11332  cvg1nlemcau  11495  cvg1nlemres  11496  rexuz3  11501  resqrexlemcvg  11530  resqrexlemglsq  11533  resqrexlemga  11534  sqrtle  11547  sqrtlt  11548  sqrt11  11550  sqrtsq2  11554  absmul  11580  sqabs  11593  abslt  11599  absle  11600  lenegsq  11606  maxleastb  11725  maxltsup  11729  rexanre  11731  negfi  11739  xrmaxiflemab  11758  xrmaxiflemlub  11759  xrmaxltsup  11769  xrmaxadd  11772  climcn2  11820  mulcn2  11823  summodclem2a  11892  summodc  11894  fsum3  11898  fsum3cvg3  11907  fsumcl2lem  11909  fsumadd  11917  fsump1i  11944  fsum0diaglem  11951  mptfzshft  11953  fsumrev  11954  fsummulc2  11959  fsum00  11973  expcnvap0  12013  mertenslemi1  12046  ntrivcvgap0  12060  prodmodclem3  12086  prodmodclem2a  12087  zproddc  12090  fprodseq  12094  fprodrev  12130  fprodconst  12131  eftlub  12201  efieq  12246  sincos1sgn  12276  demoivreALT  12285  dvdsval3  12302  dvdscmul  12329  dvdsmulc  12330  dvdscmulr  12331  dvdsmulcr  12332  modmulconst  12334  dvds2ln  12335  ltoddhalfle  12404  nn0o  12418  divalg2  12437  ndvdssub  12441  ndvdsadd  12442  divgcdz  12492  gcd0id  12500  gcdaddm  12505  bezoutlemstep  12518  bezoutlemmain  12519  dfgcd3  12531  dfgcd2  12535  lcmcllem  12589  dvdslcm  12591  lcmgcdlem  12599  lcmgcdnn  12604  qredeq  12618  qredeu  12619  rpdvds  12621  divgcdcoprm0  12623  cncongr1  12625  cncongr2  12626  cncongrcoprm  12628  prmind2  12642  isprm5  12664  isprm6  12669  prmexpb  12673  cncongrprm  12679  sqrt2irrlem  12683  pw2dvdslemn  12687  oddpwdclemxy  12691  oddpwdclemdc  12695  oddpwdc  12696  hashdvds  12743  prmdiv  12757  hashgcdlem  12760  nnoddn2prmb  12785  pythagtriplem6  12793  pythagtriplem7  12794  pcpre1  12815  pccl  12822  pcmul  12824  pcdiv  12825  pcqmul  12826  pcqcl  12829  pcdvds  12838  pcndvds  12840  pcndvds2  12842  pc2dvds  12853  dvdsprmpweqle  12860  difsqpwdvds  12861  pcaddlem  12862  pcadd  12863  pcmptcl  12865  pcmpt  12866  fldivp1  12871  pcfac  12873  oddprmdvds  12877  infpnlem2  12883  4sqlem5  12905  4sqlem6  12906  4sqlem4a  12914  4sqexercise1  12921  4sqexercise2  12922  4sqlem13m  12926  4sqlem15  12928  4sqlem16  12929  ennnfonelemfun  12988  ennnfonelemim  12995  ctinfomlemom  12998  ctinfom  12999  ctinf  13001  ctiunctlemfo  13010  omctfn  13014  fnpr2ob  13373  ismgmid2  13413  fngsum  13421  igsumvalx  13422  gsumfzval  13424  gsum0g  13429  gsumval2  13430  issgrpd  13445  ismndd  13470  prdsidlem  13480  imasmnd2  13485  mhmf1o  13503  subsubm  13516  dfgrp2  13560  isgrpid2  13573  isgrpinv  13587  grplrinv  13590  dfgrp3mlem  13631  dfgrp3m  13632  dfgrp3me  13633  prdsinvlem  13641  imasgrp2  13647  mhmmnd  13653  issubg2m  13726  issubgrpd2  13727  grpissubg  13731  subsubg  13734  subgintm  13735  isnsg3  13744  nmzsubg  13747  eqgval  13760  eqgen  13764  isghmd  13789  ghmrn  13794  ghmpreima  13803  ghmf1o  13812  conjghm  13813  conjnmzb  13817  ghmpropd  13820  rinvmod  13846  imasabl  13873  rnglz  13908  isrngd  13916  srgdilem  13932  srglmhm  13956  srgrmhm  13957  ringdilem  13975  isringd  14004  ringsrg  14010  ringinvnzdiv  14013  imasring  14027  dvdsrd  14058  unitgrp  14080  isrim0  14125  isrhm2d  14129  rhmf1o  14132  rhmco  14138  rhmopp  14140  issubrng2  14174  subsubrng  14178  subrgugrp  14204  issubrg2  14205  subsubrg  14209  resrhm  14212  aprap  14250  lmodfopnelem2  14289  lsssubg  14341  islss3  14343  islss4  14346  lspsnel6  14372  lidlacl  14448  lidlsubg  14450  lidlrsppropdg  14459  2idlelbas  14480  cnfld1  14536  cnsubglem  14543  mulgghm2  14572  zndvds  14613  mplsubgfi  14665  topgele  14703  tgcl  14738  epttop  14764  opnssneib  14830  iscnp4  14892  cnco  14895  cncnp  14904  cnrest2  14910  lmss  14920  txcnp  14945  txcn  14949  cnmpt12  14961  cnmpt22  14968  hmeof1o  14983  psmetres2  15007  distspace  15009  ismeti  15020  isxmetd  15021  xmetpsmet  15043  xblss2ps  15078  xblss2  15079  blcntrps  15089  blcntr  15090  blin2  15106  mopni3  15158  metequiv2  15170  bdmet  15176  xmettx  15184  cnbl0  15208  cnblcld  15209  tgioo  15228  elcncf1di  15253  dedekindeulemlu  15295  suplociccex  15299  dedekindicclemlu  15304  dedekindicc  15307  ivthinclemlopn  15310  ivthdec  15318  ivthreinc  15319  ivthdichlem  15325  cnplimcim  15341  limccnp2lem  15350  dvfvalap  15355  plymullem  15424  reeff1olem  15445  sin0pilem1  15455  pilem3  15457  ptolemy  15498  sincosq1sgn  15500  sinq12gt0  15504  ioocosf1o  15528  rprelogbmulexp  15630  perfectlem2  15674  lgslem3  15681  lgsne0  15717  gausslemma2dlem0b  15729  gausslemma2dlem0c  15730  lgsquadlem2  15757  lgsquad2lem2  15761  2lgsoddprmlem2  15785  2sqlem8  15802  gropd  15848  grstructd2dom  15849  incistruhgr  15890  umgrislfupgrenlem  15928  umgrislfupgrdom  15929  uspgrupgrushgr  15980  usgrumgruspgr  15983  usgruspgrben  15984  usgrislfuspgrdom  15988  umgrvad2edg  16009  umgr2edgneu  16010  ushgredgedg  16024  ushgredgedgloop  16026  iswlkg  16041  wlk2f  16062  upgriswlkdc  16071  wlkv0  16080  wlklenvclwlk  16084  bj-nnan  16100  bj-charfun  16170  bdop  16238  bdunexb  16283  bj-om  16300  findset  16308  bj-peano4  16318  bj-inf2vn  16337  bj-inf2vn2  16338  pwle2  16364  pwf1oexmid  16365  nnnninfex  16388  sbthom  16394  qdencn  16395  trilpolemlt1  16409