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  2942  eqvincg  2943  elrabd  2977  reu6  3008  reu3  3009  indifdir  3479  undif3ss  3484  un00  3557  eqifdc  3661  disjpr2  3755  prel12  3877  prneimg  3880  preqsn  3881  disjiun  4106  opth  4355  0nelop  4366  euotd  4373  opelopabsb  4380  ispod  4427  elon2  4499  unexb  4565  opeluu  4573  eusvnfb  4577  suc11g  4681  nlimsucg  4690  tfi  4706  vtoclr  4800  opthprc  4803  ideqg  4908  resiexg  5085  dminss  5179  imainss  5180  ssxpbm  5200  relrelss  5291  funopg  5388  fununfun  5401  fntpg  5414  fun11uni  5428  imain  5440  funimaexglem  5441  funssxp  5534  ffdm  5535  f00  5561  dffo2  5596  fodmrnu  5600  foco  5603  fun11iun  5637  f1o00  5653  fsnd  5661  fv3  5695  dff2  5823  dff3im  5824  dffo4  5827  ffnfv  5837  ffvresb  5842  fsn2  5853  fconstfvm  5904  fnfvima  5923  resfvresima  5925  fcof1o  5964  isocnv  5986  isotr  5991  riotaprop  6031  acexmidlemcase  6047  caovlem2d  6249  f1ocnvd  6259  caofcom  6299  resfunexgALT  6303  elxp7  6366  2ndrn  6379  1stconst  6419  2ndconst  6420  cnvf1olem  6422  poxp  6430  ressuppss  6456  funsssuppss  6460  dftpos4  6496  dfsmo2  6520  tfrlem5  6547  tfrlemiex  6564  tfr1onlemsucaccv  6574  tfr1onlembfn  6577  tfr1onlemex  6580  tfr1onlemres  6582  tfrcllemsucaccv  6587  tfrcllembfn  6590  tfrcllemex  6593  tfrcllemres  6595  tfrcl  6597  frecabex  6631  frecabcl  6632  frecfcllem  6637  frecrdg  6641  oawordi  6704  nntri3  6732  nntr2  6738  nnmordi  6751  iserd  6795  relelec  6811  erth  6815  qliftfun  6853  mapsnd  6925  mapsncnv  6932  mptelixpg  6971  bren  6985  pw2f1odclem  7089  mapunen  7106  findcard2d  7150  findcard2sd  7151  isinfinf  7156  tridc  7159  nnwetri  7178  undifdcss  7185  fiintim  7193  fisseneq  7197  fidcenumlemim  7224  sbthlemi9  7237  supisolem  7301  ordiso2  7328  updjud  7375  difinfsn  7393  ctssdccl  7404  nnnninfeq  7421  omniwomnimkv  7460  pr2cv  7496  acfun  7516  exmidontriimlem2  7531  onntri45  7553  dftap2  7567  netap  7570  2omotaplemap  7573  ccfunen  7580  cc4f  7585  cc4n  7587  elni2  7631  dfplpq2  7671  dfmpq2  7672  enqbreq2  7674  enqdc1  7679  addcmpblnq  7684  addclnq  7692  nqpi  7695  addassnqg  7699  mulassnqg  7701  mulcanenq  7702  distrnqg  7704  1qec  7705  recexnq  7707  subhalfnqq  7731  enq0tr  7751  nqnq0pi  7755  nq0nn  7759  mulcanenq0ec  7762  nnnq0lem1  7763  addclnq0  7768  distrnq0  7776  addassnq0lemcl  7778  elnp1st2nd  7793  prarloc  7820  addlocprlemlt  7848  addlocprlemeq  7850  addlocprlemgt  7851  addclpr  7854  nqprm  7859  mullocprlem  7887  mullocpr  7888  mulclpr  7889  ltpopr  7912  ltaddpr  7914  ltexprlemm  7917  ltexprlemopl  7918  ltexprlemopu  7920  ltexprlemrnd  7922  ltexprlemdisj  7923  addcanprleml  7931  addcanprlemu  7932  addcanprg  7933  recexprlemm  7941  recexprlemopl  7942  recexprlemopu  7944  recexprlemrnd  7946  recexprlemdisj  7947  cauappcvgprlemm  7962  cauappcvgprlemopl  7963  cauappcvgprlemopu  7965  cauappcvgprlemrnd  7967  cauappcvgprlemdisj  7968  cauappcvgprlemlim  7978  caucvgprlemnkj  7983  caucvgprlemm  7985  caucvgprlemopl  7986  caucvgprlemopu  7988  caucvgprlemrnd  7990  caucvgprlemlim  7998  caucvgprprlemnkltj  8006  caucvgprprlemnkeqj  8007  caucvgprprlemnjltk  8008  caucvgprprlemm  8013  caucvgprprlemopl  8014  caucvgprprlemopu  8016  caucvgprprlemrnd  8018  caucvgprprlemexbt  8023  caucvgprprlemlim  8028  suplocexprlemrl  8034  suplocexprlemru  8036  suplocexprlemdisj  8037  suplocexprlemloc  8038  suplocexprlemex  8039  suplocexprlemub  8040  prsrlem1  8059  mulclsr  8071  mulasssrg  8075  distrsrg  8076  suplocsrlemb  8123  elreal2  8147  axmulass  8190  axdistr  8191  axcaucvglemcau  8215  add20  8750  mullt0  8756  rereim  8862  ltmul1  8868  cru  8878  mulap0r  8891  aprcl  8922  aptap  8926  divmuldivap  8988  divmuleqap  8993  divadddivap  9003  divmuldivapd  9108  divmuleqapd  9109  div2subap  9113  ltmul12a  9136  lemul12a  9138  lemulge11  9142  lediv12a  9170  lediv2a  9171  recgt1i  9174  recreclt  9176  ledivp1  9179  lemul1ad  9215  lemul2ad  9216  ltmul12ad  9217  lemul12ad  9218  lemul12bd  9219  nndivre  9275  nndivtr  9281  halfaddsubcl  9473  halfaddsub  9474  lt2halves  9476  nnrecl  9496  elnn0nn  9540  elnnnn0b  9542  elnnnn0c  9543  nn0addge1  9544  nn0addge2  9545  xnn0xrnemnf  9577  elnn0z  9592  elnnz1  9602  nzadd  9632  elz2  9651  zdivadd  9670  zdivmul  9671  zextle  9672  peano2uz2  9688  uzind  9692  btwnz  9700  uzss  9878  eluzp1m1  9881  infregelbex  9933  eluz2b2  9938  qre  9960  qaddcl  9970  qmulcl  9972  qreccl  9977  irradd  9981  irrmul  9982  elpqb  9985  cnref1o  9986  rprege0  10004  rprene0  10007  rpreap0  10008  rpcnne0  10009  rpcnap0  10010  rpregt0d  10039  rprege0d  10040  rprene0d  10041  rpcnne0d  10042  lediv2ad  10055  ledivge1le  10062  lediv12ad  10092  nnledivrp  10102  nn0ledivnn  10103  xrlttri3  10133  xrrebnd  10155  xrrege0  10161  xnn0xadd0  10203  xlesubadd  10219  elioo4g  10270  ioomax  10284  iccmax  10285  divelunit  10338  elfz5  10354  uzsubsubfz  10384  fzopth  10398  fzass4  10399  fzrev2  10423  uzsplit  10430  elfz2nn0  10450  difelfzle  10472  1fv  10477  4fvwrd4  10478  fzo1fzo0n0  10526  elfzom1elp1fzo  10551  subfzo0  10592  infssuzex  10597  qtri3or  10604  adddivflid  10656  flltdivnn0lt  10668  intfracq  10686  modqid2  10717  modfzo0difsn  10761  seq3val  10826  seqvalcd  10827  iseqf1olemqcl  10865  iseqf1olemnab  10867  iseqf1olemab  10868  iseqf1olemmo  10871  seq3f1olemqsumkj  10877  seq3f1olemqsumk  10878  seqf1oglem1  10885  seqf1oglem2  10886  expclzaplem  10929  leexp1a  10960  expubnd  10962  le2sq2  10981  sumsqeq0  10984  bernneq  11026  expnlbnd  11030  nn0opthd  11088  faclbnd6  11110  facavg  11112  sseqn  11207  hashfibclem  11210  seq3coll  11218  hash2en  11219  wrdnval  11259  ccat0  11288  ccatsymb  11294  ccatalpha  11305  swrdspsleq  11363  pfxtrcfv  11389  pfxsuffeqwrdeq  11394  wrd2ind  11419  pfxccatin12lem2a  11423  pfxccatin12  11429  pfxccat3  11430  swrdccat  11431  pfxccatpfx1  11432  pfxccatpfx2  11433  swrdccatin1d  11439  swrdccatin2d  11440  shftlem  11505  shftfvalg  11507  shftfval  11510  cvg1nlemcau  11673  cvg1nlemres  11674  rexuz3  11679  resqrexlemcvg  11708  resqrexlemglsq  11711  resqrexlemga  11712  sqrtle  11725  sqrtlt  11726  sqrt11  11728  sqrtsq2  11732  absmul  11758  sqabs  11771  abslt  11777  absle  11778  lenegsq  11784  maxleastb  11903  maxltsup  11907  rexanre  11909  negfi  11917  xrmaxiflemab  11936  xrmaxiflemlub  11937  xrmaxltsup  11947  xrmaxadd  11950  climcn2  11998  mulcn2  12001  summodclem2a  12071  summodc  12073  fsum3  12077  fsum3cvg3  12086  fsumcl2lem  12088  fsumadd  12096  fsump1i  12123  fsum0diaglem  12130  mptfzshft  12132  fsumrev  12133  fsummulc2  12138  fsum00  12152  expcnvap0  12192  mertenslemi1  12225  ntrivcvgap0  12239  prodmodclem3  12265  prodmodclem2a  12266  zproddc  12269  fprodseq  12273  fprodrev  12309  fprodconst  12310  eftlub  12380  efieq  12425  sincos1sgn  12455  demoivreALT  12464  dvdsval3  12481  dvdscmul  12508  dvdsmulc  12509  dvdscmulr  12510  dvdsmulcr  12511  modmulconst  12513  dvds2ln  12514  ltoddhalfle  12583  nn0o  12597  divalg2  12616  ndvdssub  12620  ndvdsadd  12621  divgcdz  12671  gcd0id  12679  gcdaddm  12684  bezoutlemstep  12697  bezoutlemmain  12698  dfgcd3  12710  dfgcd2  12714  lcmcllem  12768  dvdslcm  12770  lcmgcdlem  12778  lcmgcdnn  12783  qredeq  12797  qredeu  12798  rpdvds  12800  divgcdcoprm0  12802  cncongr1  12804  cncongr2  12805  cncongrcoprm  12807  prmind2  12821  isprm5  12843  isprm6  12848  prmexpb  12852  cncongrprm  12858  sqrt2irrlem  12862  pw2dvdslemn  12866  oddpwdclemxy  12870  oddpwdclemdc  12874  oddpwdc  12875  hashdvds  12922  prmdiv  12936  hashgcdlem  12939  nnoddn2prmb  12964  pythagtriplem6  12972  pythagtriplem7  12973  pcpre1  12994  pccl  13001  pcmul  13003  pcdiv  13004  pcqmul  13005  pcqcl  13008  pcdvds  13017  pcndvds  13019  pcndvds2  13021  pc2dvds  13032  dvdsprmpweqle  13039  difsqpwdvds  13040  pcaddlem  13041  pcadd  13042  pcmptcl  13044  pcmpt  13045  fldivp1  13050  pcfac  13052  oddprmdvds  13056  infpnlem2  13062  4sqlem5  13084  4sqlem6  13085  4sqlem4a  13093  4sqexercise1  13100  4sqexercise2  13101  4sqlem13m  13105  4sqlem15  13107  4sqlem16  13108  ballotfilem2  13149  ballotfilemfp1  13152  ennnfonelemfun  13185  ennnfonelemim  13192  ctinfomlemom  13195  ctinfom  13196  ctinf  13198  ctiunctlemfo  13207  omctfn  13211  fnpr2ob  13570  ismgmid2  13610  fngsum  13618  igsumvalx  13619  gsumfzval  13621  gsum0g  13626  gsumval2  13627  issgrpd  13642  ismndd  13667  prdsidlem  13677  imasmnd2  13682  mhmf1o  13700  subsubm  13713  dfgrp2  13757  isgrpid2  13770  isgrpinv  13784  grplrinv  13787  dfgrp3mlem  13828  dfgrp3m  13829  dfgrp3me  13830  prdsinvlem  13838  imasgrp2  13844  mhmmnd  13850  issubg2m  13923  issubgrpd2  13924  grpissubg  13928  subsubg  13931  subgintm  13932  isnsg3  13941  nmzsubg  13944  eqgval  13957  eqgen  13961  isghmd  13986  ghmrn  13991  ghmpreima  14000  ghmf1o  14009  conjghm  14010  conjnmzb  14014  ghmpropd  14017  rinvmod  14043  imasabl  14070  rnglz  14106  isrngd  14114  srgdilem  14130  srglmhm  14154  srgrmhm  14155  ringdilem  14173  isringd  14202  ringsrg  14208  ringinvnzdiv  14211  imasring  14225  dvdsrd  14256  unitgrp  14278  isrim0  14323  isrhm2d  14327  rhmf1o  14330  rhmco  14336  rhmopp  14338  issubrng2  14372  subsubrng  14376  subrgugrp  14402  issubrg2  14403  subsubrg  14407  resrhm  14410  aprap  14449  lmodfopnelem2  14490  lsssubg  14542  islss3  14544  islss4  14547  lspsnel6  14573  lidlacl  14649  lidlsubg  14651  lidlrsppropdg  14660  2idlelbas  14681  cnfld1  14737  cnsubglem  14744  mulgghm2  14773  zndvds  14814  psrbagcon  14843  mplsubgfi  14873  topgele  14911  tgcl  14946  epttop  14972  opnssneib  15038  iscnp4  15100  cnco  15103  cncnp  15112  cnrest2  15118  lmss  15128  txcnp  15153  txcn  15157  cnmpt12  15169  cnmpt22  15176  hmeof1o  15191  psmetres2  15215  distspace  15217  ismeti  15228  isxmetd  15229  xmetpsmet  15251  xblss2ps  15286  xblss2  15287  blcntrps  15297  blcntr  15298  blin2  15314  mopni3  15366  metequiv2  15378  bdmet  15384  xmettx  15392  cnbl0  15416  cnblcld  15417  tgioo  15436  elcncf1di  15461  dedekindeulemlu  15503  suplociccex  15507  dedekindicclemlu  15512  dedekindicc  15515  ivthinclemlopn  15518  ivthdec  15526  ivthreinc  15527  ivthdichlem  15533  cnplimcim  15549  limccnp2lem  15558  dvfvalap  15563  plymullem  15632  reeff1olem  15653  sin0pilem1  15663  pilem3  15665  ptolemy  15706  sincosq1sgn  15708  sinq12gt0  15712  ioocosf1o  15736  rprelogbmulexp  15838  pellexlem3  15864  perfectlem2  15885  lgslem3  15892  lgsne0  15928  gausslemma2dlem0b  15940  gausslemma2dlem0c  15941  lgsquadlem2  15968  lgsquad2lem2  15972  2lgsoddprmlem2  15996  2sqlem8  16013  gropd  16059  grstructd2dom  16060  incistruhgr  16102  umgrislfupgrenlem  16142  umgrislfupgrdom  16143  uspgrupgrushgr  16194  usgrumgruspgr  16197  usgruspgrben  16198  usgrislfuspgrdom  16202  umgrvad2edg  16223  umgr2edgneu  16224  ushgredgedg  16238  ushgredgedgloop  16240  subgrprop3  16274  iswlkg  16341  wlk2f  16363  upgriswlkdc  16372  wlkv0  16381  wlklenvclwlk  16385  wlkepvtx  16387  upgr2wlkdc  16389  wlkres  16391  clwwlkccatlem  16412  clwwlkccat  16413  clwwlknbp  16427  clwwlknp  16429  clwwlkext2edg  16434  clwwlknon  16441  clwwlknonccat  16445  clwwlknonex2  16451  clwwlknonex2e  16452  trlsegvdeglem1  16472  bj-nnan  16525  bj-charfun  16594  bdop  16662  bdunexb  16707  bj-om  16724  findset  16732  bj-peano4  16742  bj-inf2vn  16761  bj-inf2vn2  16762  pwle2  16789  pwf1oexmid  16790  nnnninfex  16817  sbthom  16823  qdencn  16824  trilpolemlt1  16842  gfsumval  16879  gfsump1  16885