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  1778  sbcof2  1859  sbequ8  1896  eu2  2127  eu3h  2128  eu5  2130  mooran2  2156  datisi  2193  felapton  2197  darapti  2198  dimatis  2200  fresison  2201  fesapo  2203  reximssdv  2648  r19.26  2671  r19.29af2  2685  r19.40  2699  eqvinc  2943  eqvincg  2944  elrabd  2978  reu6  3009  reu3  3010  indifdir  3481  undif3ss  3486  un00  3556  vvin  3558  eqifdc  3664  disjpr2  3759  prel12  3881  prneimg  3884  preqsn  3885  disjiun  4110  opth  4359  0nelop  4370  euotd  4377  opelopabsb  4384  ispod  4431  elon2  4503  unexb  4570  opeluu  4578  eusvnfb  4582  suc11g  4686  nlimsucg  4695  tfi  4711  vtoclr  4805  opthprc  4808  ideqg  4913  resiexg  5090  dminss  5184  imainss  5185  ssxpbm  5205  relrelss  5296  funopg  5393  fununfun  5406  fntpg  5419  fun11uni  5433  imain  5445  funimaexglem  5446  funssxp  5539  ffdm  5540  f00  5566  dffo2  5601  fodmrnu  5605  foco  5608  fun11iun  5642  f1o00  5658  fsnd  5666  fv3  5700  dff2  5828  dff3im  5829  dffo4  5832  ffnfv  5842  ffvresb  5847  fsn2  5858  fconstfvm  5909  fnfvima  5928  resfvresima  5931  fcof1o  5970  isocnv  5992  isotr  5997  riotaprop  6039  acexmidlemcase  6055  caovlem2d  6257  f1ocnvd  6267  f1o3d  6273  caofcom  6308  resfunexgALT  6312  elxp7  6379  2ndrn  6392  1stconst  6432  2ndconst  6433  cnvf1olem  6435  poxp  6443  ressuppss  6469  funsssuppss  6473  dftpos4  6509  dfsmo2  6533  tfrlem5  6560  tfrlemiex  6577  tfr1onlemsucaccv  6587  tfr1onlembfn  6590  tfr1onlemex  6593  tfr1onlemres  6595  tfrcllemsucaccv  6600  tfrcllembfn  6603  tfrcllemex  6606  tfrcllemres  6608  tfrcl  6610  frecabex  6644  frecabcl  6645  frecfcllem  6650  frecrdg  6654  oawordi  6717  nntri3  6745  nntr2  6751  nnmordi  6764  iserd  6808  relelec  6824  erth  6828  qliftfun  6866  mapsnd  6938  mapsncnv  6945  mptelixpg  6984  bren  6998  pw2f1odclem  7102  mapunen  7119  findcard2d  7163  findcard2sd  7164  isinfinf  7169  tridc  7172  nnwetri  7191  undifdcss  7198  fiintim  7206  fisseneq  7210  fidcenumlemim  7237  sbthlemi9  7250  supisolem  7314  ordiso2  7341  updjud  7388  difinfsn  7406  ctssdccl  7417  nnnninfeq  7434  omniwomnimkv  7473  pr2cv  7509  acfun  7529  exmidontriimlem2  7544  onntri45  7566  dftap2  7583  netap  7586  2omotaplemap  7589  ccfunen  7596  cc4f  7601  cc4n  7603  elni2  7647  dfplpq2  7687  dfmpq2  7688  enqbreq2  7690  enqdc1  7695  addcmpblnq  7700  addclnq  7708  nqpi  7711  addassnqg  7715  mulassnqg  7717  mulcanenq  7718  distrnqg  7720  1qec  7721  recexnq  7723  subhalfnqq  7747  enq0tr  7767  nqnq0pi  7771  nq0nn  7775  mulcanenq0ec  7778  nnnq0lem1  7779  addclnq0  7784  distrnq0  7792  addassnq0lemcl  7794  elnp1st2nd  7809  prarloc  7836  addlocprlemlt  7864  addlocprlemeq  7866  addlocprlemgt  7867  addclpr  7870  nqprm  7875  mullocprlem  7903  mullocpr  7904  mulclpr  7905  ltpopr  7928  ltaddpr  7930  ltexprlemm  7933  ltexprlemopl  7934  ltexprlemopu  7936  ltexprlemrnd  7938  ltexprlemdisj  7939  addcanprleml  7947  addcanprlemu  7948  addcanprg  7949  recexprlemm  7957  recexprlemopl  7958  recexprlemopu  7960  recexprlemrnd  7962  recexprlemdisj  7963  cauappcvgprlemm  7978  cauappcvgprlemopl  7979  cauappcvgprlemopu  7981  cauappcvgprlemrnd  7983  cauappcvgprlemdisj  7984  cauappcvgprlemlim  7994  caucvgprlemnkj  7999  caucvgprlemm  8001  caucvgprlemopl  8002  caucvgprlemopu  8004  caucvgprlemrnd  8006  caucvgprlemlim  8014  caucvgprprlemnkltj  8022  caucvgprprlemnkeqj  8023  caucvgprprlemnjltk  8024  caucvgprprlemm  8029  caucvgprprlemopl  8030  caucvgprprlemopu  8032  caucvgprprlemrnd  8034  caucvgprprlemexbt  8039  caucvgprprlemlim  8044  suplocexprlemrl  8050  suplocexprlemru  8052  suplocexprlemdisj  8053  suplocexprlemloc  8054  suplocexprlemex  8055  suplocexprlemub  8056  prsrlem1  8075  mulclsr  8087  mulasssrg  8091  distrsrg  8092  suplocsrlemb  8139  elreal2  8163  axmulass  8206  axdistr  8207  axcaucvglemcau  8231  add20  8768  mullt0  8774  rereim  8880  ltmul1  8886  cru  8896  mulap0r  8909  aprcl  8940  aptap  8944  divmuldivap  9008  divmuleqap  9013  divadddivap  9023  divmuldivapd  9128  divmuleqapd  9129  div2subap  9133  ltmul12a  9156  lemul12a  9158  lemulge11  9162  lediv12a  9190  lediv2a  9191  recgt1i  9194  recreclt  9196  ledivp1  9199  lemul1ad  9235  lemul2ad  9236  ltmul12ad  9237  lemul12ad  9238  lemul12bd  9239  nndivre  9295  nndivtr  9301  halfaddsubcl  9493  halfaddsub  9494  lt2halves  9496  nnrecl  9516  elnn0nn  9560  elnnnn0b  9562  elnnnn0c  9563  nn0addge1  9564  nn0addge2  9565  xnn0xrnemnf  9597  elnn0z  9612  elnnz1  9622  nzadd  9652  elz2  9671  zdivadd  9690  zdivmul  9691  zextle  9692  peano2uz2  9708  uzind  9712  btwnz  9720  uzss  9898  eluzp1m1  9901  infregelbex  9953  eluz2b2  9958  qre  9980  qaddcl  9990  qmulcl  9992  qreccl  9997  irradd  10001  irrmul  10002  elpqb  10005  cnref1o  10006  rprege0  10024  rprene0  10027  rpreap0  10028  rpcnne0  10029  rpcnap0  10030  rpregt0d  10059  rprege0d  10060  rprene0d  10061  rpcnne0d  10062  lediv2ad  10075  ledivge1le  10082  lediv12ad  10112  nnledivrp  10122  nn0ledivnn  10123  xrlttri3  10154  xrrebnd  10176  xrrege0  10182  xnn0xadd0  10224  xlesubadd  10240  elioo4g  10291  ioomax  10305  iccmax  10306  divelunit  10359  elfz5  10375  uzsubsubfz  10406  fzopth  10421  fzass4  10422  fzrev2  10446  uzsplit  10453  elfz2nn0  10473  difelfzle  10495  1fv  10500  4fvwrd4  10501  fzo1fzo0n0  10549  elfzom1elp1fzo  10574  subfzo0  10615  infssuzex  10620  infssfzcldc  10623  infssfzledc  10624  qtri3or  10629  adddivflid  10681  flltdivnn0lt  10693  intfracq  10711  modqid2  10742  modfzo0difsn  10786  seq3val  10851  seqvalcd  10852  iseqf1olemqcl  10890  iseqf1olemnab  10892  iseqf1olemab  10893  iseqf1olemmo  10896  seq3f1olemqsumkj  10902  seq3f1olemqsumk  10903  seqf1oglem1  10910  seqf1oglem2  10911  expclzaplem  10954  leexp1a  10985  expubnd  10987  le2sq2  11006  sumsqeq0  11009  bernneq  11052  expnlbnd  11056  nn0opthd  11114  faclbnd6  11136  facavg  11138  sseqn  11233  hashfibclem  11236  seq3coll  11244  hash2en  11245  wrdnval  11285  ccat0  11314  ccatsymb  11320  ccatalpha  11331  swrdspsleq  11389  pfxtrcfv  11415  pfxsuffeqwrdeq  11420  wrd2ind  11445  pfxccatin12lem2a  11449  pfxccatin12  11455  pfxccat3  11456  swrdccat  11457  pfxccatpfx1  11458  pfxccatpfx2  11459  swrdccatin1d  11465  swrdccatin2d  11466  shftlem  11531  shftfvalg  11533  shftfval  11536  cvg1nlemcau  11700  cvg1nlemres  11701  rexuz3  11706  resqrexlemcvg  11735  resqrexlemglsq  11738  resqrexlemga  11739  sqrtle  11752  sqrtlt  11753  sqrt11  11755  sqrtsq2  11759  absmul  11785  sqabs  11798  abslt  11804  absle  11805  lenegsq  11811  maxleastb  11930  maxltsup  11934  rexanre  11936  negfi  11944  xrmaxiflemab  11963  xrmaxiflemlub  11964  xrmaxltsup  11974  xrmaxadd  11977  climcn2  12025  mulcn2  12028  summodclem2a  12098  summodc  12100  fsum3  12104  fsum3cvg3  12113  fsumcl2lem  12115  fsumadd  12123  fsump1i  12150  fsum0diaglem  12157  mptfzshft  12159  fsumrev  12160  fsummulc2  12165  fsum00  12179  expcnvap0  12219  mertenslemi1  12252  ntrivcvgap0  12266  prodmodclem3  12292  prodmodclem2a  12293  zproddc  12296  fprodseq  12300  fprodrev  12336  fprodconst  12337  eftlub  12407  efieq  12452  sincos1sgn  12482  demoivreALT  12491  dvdsval3  12508  dvdscmul  12535  dvdsmulc  12536  dvdscmulr  12537  dvdsmulcr  12538  modmulconst  12540  dvds2ln  12541  ltoddhalfle  12610  nn0o  12624  divalg2  12643  ndvdssub  12647  ndvdsadd  12648  divgcdz  12698  gcd0id  12706  gcdaddm  12711  bezoutlemstep  12724  bezoutlemmain  12725  dfgcd3  12737  dfgcd2  12741  lcmcllem  12795  dvdslcm  12797  lcmgcdlem  12805  lcmgcdnn  12810  qredeq  12824  qredeu  12825  rpdvds  12827  divgcdcoprm0  12829  cncongr1  12831  cncongr2  12832  cncongrcoprm  12834  prmind2  12848  isprm5  12870  isprm6  12875  prmexpb  12879  cncongrprm  12885  sqrt2irrlem  12889  pw2dvdslemn  12893  oddpwdclemxy  12897  oddpwdclemdc  12901  oddpwdc  12902  hashdvds  12949  prmdiv  12963  hashgcdlem  12966  nnoddn2prmb  12991  pythagtriplem6  12999  pythagtriplem7  13000  pcpre1  13021  pccl  13028  pcmul  13030  pcdiv  13031  pcqmul  13032  pcqcl  13035  pcdvds  13044  pcndvds  13046  pcndvds2  13048  pc2dvds  13059  dvdsprmpweqle  13066  difsqpwdvds  13067  pcaddlem  13068  pcadd  13069  pcmptcl  13071  pcmpt  13072  fldivp1  13077  pcfac  13079  oddprmdvds  13083  infpnlem2  13089  4sqlem5  13111  4sqlem6  13112  4sqlem4a  13120  4sqexercise1  13127  4sqexercise2  13128  4sqlem13m  13132  4sqlem15  13134  4sqlem16  13135  ballotfilem2  13178  ballotfilemfp1  13181  ballotfilemsf1o  13207  ballotfilemrinv0  13226  ballotfilem7  13229  ballotfilemth  13231  ennnfonelemfun  13258  ennnfonelemim  13265  ctinfomlemom  13268  ctinfom  13269  ctinf  13271  ctiunctlemfo  13280  omctfn  13284  fnpr2ob  13610  ismgmid2  13649  fngzsum  13657  gzsumvalx  13658  gzsumfzval  13660  gzsum0  13662  gzsumval2  13663  issgrpd  13676  ismndd  13699  imasmnd2  13708  mhmf1o  13726  subsubm  13739  dfgrp2  13781  isgrpid2  13794  isgrpinv  13808  grplrinv  13811  dfgrp3mlem  13852  dfgrp3m  13853  dfgrp3me  13854  imasgrp2  13862  mhmmnd  13868  issubg2m  13941  issubgrpd2  13942  grpissubg  13946  subsubg  13949  subgintm  13950  isnsg3  13959  nmzsubg  13962  eqgval  13975  eqgen  13979  isghmd  14004  ghmrn  14009  ghmpreima  14018  ghmf1o  14027  conjghm  14028  conjnmzb  14032  ghmpropd  14035  rinvmod  14062  imasabl  14089  gsumvalfi  14101  gsump1  14106  prdsidlem  14142  prdsinvlem  14145  rnglz  14191  isrngd  14199  rng1zr  14206  srgdilem  14219  srg1zr  14237  srglmhm  14243  srgrmhm  14244  ringdilem  14262  isringd  14291  ringsrg  14297  ringinvnzdiv  14300  imasring  14314  dvdsrd  14346  unitgrp  14368  isrim0  14413  isrhm2d  14417  rhmf1o  14420  rhmco  14426  rhmopp  14428  issubrng2  14463  subsubrng  14467  subrgugrp  14493  issubrg2  14494  subsubrg  14498  resrhm  14501  ringunitap  14538  aprap  14543  drngunitap  14553  lmodfopnelem2  14606  lsssubg  14658  islss3  14660  islss4  14663  lspsnel6  14689  lidlacl  14765  lidlsubg  14767  lidlrsppropdg  14776  2idlelbas  14797  cnfld1  14853  cnsubglem  14860  mulgghm2  14887  zndvds  14928  psrbagcon  14957  mplsubgfi  14987  topgele  15025  tgcl  15060  epttop  15086  opnssneib  15152  iscnp4  15214  cnco  15217  cncnp  15226  cnrest2  15232  lmss  15242  txcnp  15267  txcn  15271  cnmpt12  15283  cnmpt22  15290  hmeof1o  15305  psmetres2  15329  distspace  15331  ismeti  15342  isxmetd  15343  xmetpsmet  15365  xblss2ps  15400  xblss2  15401  blcntrps  15411  blcntr  15412  blin2  15428  mopni3  15480  metequiv2  15492  bdmet  15498  xmettx  15506  cnbl0  15530  cnblcld  15531  tgioo  15550  elcncf1di  15575  dedekindeulemlu  15617  suplociccex  15621  dedekindicclemlu  15626  dedekindicc  15629  ivthinclemlopn  15632  ivthdec  15640  ivthreinc  15641  ivthdichlem  15647  cnplimcim  15663  limccnp2lem  15672  dvfvalap  15677  plymullem  15746  reeff1olem  15767  sin0pilem1  15777  pilem3  15779  ptolemy  15820  sincosq1sgn  15822  sinq12gt0  15826  ioocosf1o  15850  rprelogbmulexp  15952  pellexlem3  15978  perfectlem2  15999  lgslem3  16006  lgsne0  16042  gausslemma2dlem0b  16054  gausslemma2dlem0c  16055  lgsquadlem2  16082  lgsquad2lem2  16086  2lgsoddprmlem2  16110  2sqlem8  16127  gropd  16173  grstructd2dom  16174  incistruhgr  16216  umgrislfupgrenlem  16256  umgrislfupgrdom  16257  uspgrupgrushgr  16308  usgrumgruspgr  16311  usgruspgrben  16312  usgrislfuspgrdom  16316  umgrvad2edg  16337  umgr2edgneu  16338  ushgredgedg  16352  ushgredgedgloop  16354  subgrprop3  16388  iswlkg  16455  wlk2f  16477  upgriswlkdc  16486  wlkv0  16495  wlklenvclwlk  16499  wlkepvtx  16501  upgr2wlkdc  16503  wlkres  16505  clwwlkccatlem  16526  clwwlkccat  16527  clwwlknbp  16541  clwwlknp  16543  clwwlkext2edg  16548  clwwlknon  16555  clwwlknonccat  16559  clwwlknonex2  16565  clwwlknonex2e  16566  trlsegvdeglem1  16586  dichmul0orlem3  16640  bj-nnan  16649  bj-charfun  16718  bdop  16786  bdunexb  16831  bj-om  16848  findset  16856  bj-peano4  16866  bj-inf2vn  16885  bj-inf2vn2  16886  pwle2  16913  pwf1oexmid  16914  nnnninfex  16941  sbthom  16947  qdencn  16948  trilpolemlt1  16966