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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jca31  309  jca32  310  jcai  311  jctil  312  jctir  313  ancli  323  ancri  324  sylanbrc  421  jcab  611  biadanid  622  ioran  764  ordi  828  stdcndc  857  stdcndcOLD  858  dfandc  896  mpbi2and  956  mpbir2and  957  pm4.82  963  pm4.83dc  964  rnlem  989  ifp2  993  syl22anc  1279  syl112anc  1282  syl121anc  1283  syl211anc  1284  syl23anc  1285  syl32anc  1286  syl122anc  1287  syl212anc  1288  syl221anc  1289  syl222anc  1294  syl123anc  1295  syl132anc  1296  syl213anc  1297  syl231anc  1298  syl312anc  1299  syl321anc  1300  syl223anc  1304  syl232anc  1305  syl322anc  1306  syl233anc  1307  syl323anc  1308  syl332anc  1309  ecased  1390  19.26  1534  nfand  1621  19.40  1684  equsexd  1782  sbcof2  1863  sbequ8  1900  eu2  2131  eu3h  2132  eu5  2134  mooran2  2160  datisi  2197  felapton  2201  darapti  2202  dimatis  2204  fresison  2205  fesapo  2207  reximssdv  2654  r19.26  2677  r19.29af2  2691  r19.40  2705  eqvinc  2949  eqvincg  2950  elrabd  2984  reu6  3015  reu3  3016  indifdir  3487  undif3ss  3492  un00  3567  vvin  3569  eqifdc  3677  disjpr2  3773  prel12  3896  prneimg  3899  preqsn  3900  disjiun  4125  opth  4377  0nelop  4388  euotd  4395  opelopabsb  4402  ispod  4449  elon2  4521  unexb  4588  opeluu  4596  eusvnfb  4600  suc11g  4704  nlimsucg  4713  tfi  4729  vtoclr  4823  opthprc  4826  ideqg  4931  resiexg  5108  dminss  5202  imainss  5203  ssxpbm  5223  relrelss  5314  funopg  5411  fununfun  5424  fntpg  5437  fun11uni  5451  imain  5463  funimaexglem  5464  funssxp  5557  ffdm  5558  f00  5584  dffo2  5619  fodmrnu  5623  foco  5626  fun11iun  5660  f1o00  5676  fsnd  5684  fv3  5718  fvun1d  5771  fvun2d  5772  dff2  5852  dff3im  5853  dffo4  5856  ffnfv  5866  ffvresb  5871  fsn2  5882  fconstfvm  5933  fnfvima  5953  resfvresima  5956  fcof1o  5995  isocnv  6017  isotr  6022  riotaprop  6064  acexmidlemcase  6080  caovlem2d  6282  f1ocnvd  6292  f1o3d  6298  caofcom  6333  resfunexgALT  6337  elxp7  6404  2ndrn  6417  1stconst  6457  2ndconst  6458  cnvf1olem  6460  poxp  6468  ressuppss  6494  funsssuppss  6498  dftpos4  6534  dfsmo2  6558  tfrlem5  6585  tfrlemiex  6602  tfr1onlemsucaccv  6612  tfr1onlembfn  6615  tfr1onlemex  6618  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembfn  6628  tfrcllemex  6631  tfrcllemres  6633  tfrcl  6635  frecabex  6669  frecabcl  6670  frecfcllem  6675  frecrdg  6679  oawordi  6742  nntri3  6770  nntr2  6776  nnmordi  6789  iserd  6833  relelec  6849  erth  6853  qliftfun  6891  mapsnd  6970  mapsncnv  6977  mptelixpg  7016  bren  7030  pw2f1odclem  7134  mapunen  7151  findcard2d  7195  findcard2sd  7196  isinfinf  7201  tridc  7204  nnwetri  7223  undifdcss  7230  fiintim  7238  fisseneq  7242  fidcenumlemim  7269  sbthlemi9  7282  supisolem  7348  ordiso2  7375  updjud  7422  difinfsn  7440  ctssdccl  7451  nnnninfeq  7468  omniwomnimkv  7507  pr2cv  7543  acfun  7563  exmidontriimlem2  7578  onntri45  7600  dftap2  7617  netap  7620  2omotaplemap  7623  ccfunen  7630  cc4f  7635  cc4n  7637  elni2  7681  dfplpq2  7721  dfmpq2  7722  enqbreq2  7724  enqdc1  7729  addcmpblnq  7734  addclnq  7742  nqpi  7745  addassnqg  7749  mulassnqg  7751  mulcanenq  7752  distrnqg  7754  1qec  7755  recexnq  7757  subhalfnqq  7781  enq0tr  7801  nqnq0pi  7805  nq0nn  7809  mulcanenq0ec  7812  nnnq0lem1  7813  addclnq0  7818  distrnq0  7826  addassnq0lemcl  7828  elnp1st2nd  7843  prarloc  7870  addlocprlemlt  7898  addlocprlemeq  7900  addlocprlemgt  7901  addclpr  7904  nqprm  7909  mullocprlem  7937  mullocpr  7938  mulclpr  7939  ltpopr  7962  ltaddpr  7964  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemrnd  7972  ltexprlemdisj  7973  addcanprleml  7981  addcanprlemu  7982  addcanprg  7983  recexprlemm  7991  recexprlemopl  7992  recexprlemopu  7994  recexprlemrnd  7996  recexprlemdisj  7997  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemrnd  8017  cauappcvgprlemdisj  8018  cauappcvgprlemlim  8028  caucvgprlemnkj  8033  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemrnd  8040  caucvgprlemlim  8048  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnjltk  8058  caucvgprprlemm  8063  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemrnd  8068  caucvgprprlemexbt  8073  caucvgprprlemlim  8078  suplocexprlemrl  8084  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  prsrlem1  8109  mulclsr  8121  mulasssrg  8125  distrsrg  8126  suplocsrlemb  8173  elreal2  8197  axmulass  8240  axdistr  8241  axcaucvglemcau  8265  add20  8803  mullt0  8809  rereim  8916  ltmul1  8922  cru  8932  mulap0r  8945  aprcl  8976  aptap  8980  divmuldivap  9044  divmuleqap  9049  divadddivap  9059  divmuldivapd  9164  divmuleqapd  9165  div2subap  9169  ltmul12a  9192  lemul12a  9194  lemulge11  9198  lediv12a  9226  lediv2a  9227  recgt1i  9230  recreclt  9232  ledivp1  9235  lemul1ad  9271  lemul2ad  9272  ltmul12ad  9273  lemul12ad  9274  lemul12bd  9275  nndivre  9342  nndivtr  9348  halfaddsubcl  9542  halfaddsub  9543  lt2halves  9545  nnrecl  9565  elnn0nn  9609  elnnnn0b  9611  elnnnn0c  9612  nn0addge1  9613  nn0addge2  9614  xnn0xrnemnf  9646  elnn0z  9661  elnnz1  9671  nzadd  9701  elz2  9720  zdivadd  9739  zdivmul  9740  zextle  9741  peano2uz2  9757  uzind  9761  btwnz  9769  uzss  9952  eluzp1m1  9955  infregelbex  10007  eluz2b2  10012  qre  10034  qaddcl  10044  qmulcl  10046  qreccl  10051  irradd  10055  irraddap  10056  irrmul  10057  elpqb  10060  cnref1o  10061  rprege0  10079  rprene0  10082  rpreap0  10083  rpcnne0  10084  rpcnap0  10085  rpregt0d  10114  rprege0d  10115  rprene0d  10116  rpcnne0d  10117  lediv2ad  10130  ledivge1le  10137  lediv12ad  10167  nnledivrp  10177  nn0ledivnn  10178  xrlttri3  10209  xrrebnd  10231  xrrege0  10237  xnn0xadd0  10279  xlesubadd  10295  elioo4g  10346  ioomax  10360  iccmax  10361  divelunit  10414  elfz5  10430  uzsubsubfz  10462  fzopth  10477  fzass4  10478  fzrev2  10502  uzsplit  10509  elfz2nn0  10529  difelfzle  10551  1fv  10556  4fvwrd4  10557  fzo1fzo0n0  10605  elfzom1elp1fzo  10630  subfzo0  10671  infssuzex  10676  infssfzcldc  10679  infssfzledc  10680  qtri3or  10685  adddivflid  10740  flltdivnn0lt  10752  intfracq  10770  modqid2  10801  modfzo0difsn  10845  seq3val  10910  seqvalcd  10911  iseqf1olemqcl  10949  iseqf1olemnab  10951  iseqf1olemab  10952  iseqf1olemmo  10955  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seqf1oglem1  10969  seqf1oglem2  10970  expclzaplem  11013  leexp1a  11044  expubnd  11046  le2sq2  11065  sumsqeq0  11068  bernneq  11111  expnlbnd  11115  nn0sqdc  11160  nn0opthd  11174  faclbnd6  11196  facavg  11198  sseqn  11293  hashfibclem  11296  hashf1lem2  11300  seq3coll  11308  hash2en  11309  wrdnval  11349  ccat0  11378  ccatsymb  11384  ccatalpha  11395  swrdspsleq  11453  pfxtrcfv  11479  pfxsuffeqwrdeq  11484  wrd2ind  11509  pfxccatin12lem2a  11513  pfxccatin12  11519  pfxccat3  11520  swrdccat  11521  pfxccatpfx1  11522  pfxccatpfx2  11523  swrdccatin1d  11529  swrdccatin2d  11530  shftlem  11595  shftfvalg  11597  shftfval  11600  cvg1nlemcau  11764  cvg1nlemres  11765  rexuz3  11770  resqrexlemcvg  11799  resqrexlemglsq  11802  resqrexlemga  11803  sqrtle  11816  sqrtlt  11817  sqrt11  11819  sqrtsq2  11823  absmul  11849  sqabs  11863  abslt  11869  absle  11870  lenegsq  11876  maxleastb  11995  maxltsup  11999  rexanre  12001  negfi  12009  xrmaxiflemab  12029  xrmaxiflemlub  12030  xrmaxltsup  12040  xrmaxadd  12043  climcn2  12091  mulcn2  12094  summodclem2a  12164  summodc  12166  fsum3  12170  fsum3cvg3  12179  fsumcl2lem  12181  fsumadd  12189  fsump1i  12216  fsum0diaglem  12223  mptfzshft  12225  fsumrev  12226  fsummulc2  12231  fsum00  12245  expcnvap0  12285  mertenslemi1  12318  ntrivcvgap0  12332  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  fprodrev  12402  fprodconst  12403  eftlub  12473  efieq  12518  sincos1sgn  12548  demoivreALT  12557  dvdsval3  12574  dvdscmul  12601  dvdsmulc  12602  dvdscmulr  12603  dvdsmulcr  12604  modmulconst  12606  dvds2ln  12607  ltoddhalfle  12676  nn0o  12690  divalg2  12709  ndvdssub  12713  ndvdsadd  12714  divgcdz  12764  gcd0id  12772  gcdaddm  12777  bezoutlemstep  12790  bezoutlemmain  12791  dfgcd3  12803  dfgcd2  12807  lcmcllem  12861  dvdslcm  12863  lcmgcdlem  12871  lcmgcdnn  12876  qredeq  12890  qredeu  12891  rpdvds  12893  divgcdcoprm0  12895  cncongr1  12897  cncongr2  12898  cncongrcoprm  12900  prmind2  12914  isprm5  12937  isprm6  12942  prmexpb  12946  cncongrprm  12952  sqrt2irrlem  12956  pwbdvdslemn  12960  nnmaxpwlemxy  12964  nnmaxpwlemparts  12968  nnmaxpw  12969  hashdvds  13019  prmdiv  13033  hashgcdlem  13036  nnoddn2prmb  13061  pythagtriplem6  13069  pythagtriplem7  13070  pcpre1  13091  pccl  13098  pcmul  13100  pcdiv  13101  pcqmul  13102  pcqcl  13105  pcdvds  13114  pcndvds  13116  pcndvds2  13118  pc2dvds  13129  dvdsprmpweqle  13136  difsqpwdvds  13137  pcaddlem  13138  pcadd  13139  pcmptcl  13141  pcmpt  13142  fldivp1  13147  pcfac  13149  oddprmdvds  13153  infpnlem2  13159  4sqlem5  13181  4sqlem6  13182  4sqlem4a  13190  4sqexercise1  13197  4sqexercise2  13198  4sqlem13m  13202  4sqlem15  13204  4sqlem16  13205  ballotfilem2  13277  ballotfilemfp1  13280  ballotfilemsf1o  13306  ballotfilemrinv0  13325  ballotfilem7  13328  ballotfilemth  13330  ennnfonelemfun  13357  ennnfonelemim  13364  ctinfomlemom  13367  ctinfom  13368  ctinf  13370  ctiunctlemfo  13379  omctfn  13383  fnpr2ob  13710  ismgmid2  13749  fngzsum  13757  gzsumvalx  13758  gzsumfzval  13760  gzsum0  13762  gzsumval2  13763  issgrpd  13776  ismndd  13799  imasmnd2  13808  mhmf1o  13826  subsubm  13839  dfgrp2  13881  isgrpid2  13894  isgrpinv  13908  grplrinv  13911  dfgrp3mlem  13952  dfgrp3m  13953  dfgrp3me  13954  imasgrp2  13962  mhmmnd  13968  issubg2m  14041  issubgrpd2  14042  grpissubg  14046  subsubg  14049  subgintm  14050  isnsg3  14059  nmzsubg  14062  eqgval  14075  eqgen  14079  isghmd  14104  ghmrn  14109  ghmpreima  14118  ghmf1o  14127  conjghm  14128  conjnmzb  14132  ghmpropd  14135  rinvmod  14162  imasabl  14189  gsumvalfi  14201  gsump1  14206  prdsidlem  14242  prdsinvlem  14245  rnglz  14293  isrngd  14301  rng1zr  14308  srgdilem  14322  srg1zr  14340  srglmhm  14346  srgrmhm  14347  ringdilem  14365  isringd  14395  ringsrg  14401  ringinvnzdiv  14404  imasring  14418  dvdsrd  14450  unitgrp  14472  isrim0  14517  isrhm2d  14521  rhmf1o  14524  rhmco  14530  rhmopp  14532  issubrng2  14567  subsubrng  14571  subrgugrp  14597  issubrg2  14598  subsubrg  14602  resrhm  14605  ringunitap  14642  aprap  14647  drngunitap  14657  lmodfopnelem2  14711  lsssubg  14763  islss3  14765  islss4  14768  ellspsn6  14794  lidlacl  14870  lidlsubg  14872  lidlrsppropdg  14881  2idlelbas  14902  cnfld1  14958  cnsubglem  14965  mulgghm2  14992  zndvds  15033  isassad  15060  issubassa  15062  assapropd  15063  psrbagcon  15111  mplsubgfi  15141  topgele  15179  tgcl  15214  epttop  15240  opnssneib  15306  iscnp4  15368  cnco  15371  cncnp  15380  cnrest2  15386  lmss  15396  txcnp  15421  txcn  15425  cnmpt12  15437  cnmpt22  15444  hmeof1o  15459  psmetres2  15483  distspace  15485  ismeti  15496  isxmetd  15497  xmetpsmet  15519  xblss2ps  15554  xblss2  15555  blcntrps  15565  blcntr  15566  blin2  15582  mopni3  15634  metequiv2  15646  bdmet  15652  xmettx  15660  cnbl0  15684  cnblcld  15685  tgioo  15704  elcncf1di  15729  dedekindeulemlu  15771  suplociccex  15775  dedekindicclemlu  15780  dedekindicc  15783  ivthinclemlopn  15786  ivthdec  15794  ivthreinc  15795  ivthdichlem  15801  cnplimcim  15817  limccnp2lem  15826  dvfvalap  15831  plymullem  15900  reeff1olem  15921  sin0pilem1  15932  pilem3  15934  ptolemy  15975  sincosq1sgn  15977  sinq12gt0  15981  ioocosf1o  16005  rprelogbmulexp  16111  zprmlogbaplem2  16135  pellexlem3  16150  perfectlem2  16198  bcmono  16202  bclbnd  16205  bposlem5  16213  lgslem3  16219  lgsne0  16255  gausslemma2dlem0b  16267  gausslemma2dlem0c  16268  lgsquadlem2  16295  lgsquad2lem2  16299  2lgsoddprmlem2  16323  2sqlem8  16340  gropd  16386  grstructd2dom  16387  incistruhgr  16429  umgrislfupgrenlem  16469  umgrislfupgrdom  16470  uspgrupgrushgr  16521  usgrumgruspgr  16524  usgruspgrben  16525  usgrislfuspgrdom  16529  umgrvad2edg  16550  umgr2edgneu  16551  ushgredgedg  16565  ushgredgedgloop  16567  subgrprop3  16601  iswlkg  16668  wlk2f  16690  upgriswlkdc  16699  wlkv0  16708  wlklenvclwlk  16712  wlkepvtx  16714  upgr2wlkdc  16716  wlkres  16718  clwwlkccatlem  16739  clwwlkccat  16740  clwwlknbp  16754  clwwlknp  16756  clwwlkext2edg  16761  clwwlknon  16768  clwwlknonccat  16772  clwwlknonex2  16778  clwwlknonex2e  16779  trlsegvdeglem1  16799  dichmul0orlem3  16853  bj-nnan  16862  bj-charfun  16931  bdop  16999  bdunexb  17044  bj-om  17061  findset  17069  bj-peano4  17079  bj-inf2vn  17098  bj-inf2vn2  17099  pwle2  17126  pwf1oexmid  17127  nnnninfex  17163  sbthom  17169  qdencn  17170  trilpolemlt1  17188