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	⊢ (𝜑 → 𝜓)
jca.2	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
jca	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Proof of Theorem jca

Step	Hyp	Ref	Expression
1		jca.1	. 2 ⊢ (𝜑 → 𝜓)
2		jca.2	. 2 ⊢ (𝜑 → 𝜒)
3		pm3.2 139	. 2 ⊢ (𝜓 → (𝜒 → (𝜓 ∧ 𝜒)))
4	1, 2, 3	sylc 62	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

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  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  2637  r19.26  2660  r19.29af2  2674  r19.40  2688  eqvinc  2930  eqvincg  2931  elrabd  2965  reu6  2996  reu3  2997  indifdir  3465  undif3ss  3470  un00  3543  eqifdc  3646  disjpr2  3737  prel12  3859  prneimg  3862  preqsn  3863  disjiun  4088  opth  4335  0nelop  4346  euotd  4353  opelopabsb  4360  ispod  4407  elon2  4479  unexb  4545  opeluu  4553  eusvnfb  4557  suc11g  4661  nlimsucg  4670  tfi  4686  vtoclr  4780  opthprc  4783  ideqg  4887  resiexg  5064  dminss  5158  imainss  5159  ssxpbm  5179  relrelss  5270  funopg  5367  fununfun  5380  fntpg  5393  fun11uni  5407  imain  5419  funimaexglem  5420  funssxp  5512  ffdm  5513  f00  5537  dffo2  5572  fodmrnu  5576  foco  5579  fun11iun  5613  f1o00  5629  fsnd  5637  fv3  5671  dff2  5799  dff3im  5800  dffo4  5803  ffnfv  5813  ffvresb  5818  fsn2  5829  fconstfvm  5880  fnfvima  5899  resfvresima  5901  fcof1o  5940  isocnv  5962  isotr  5967  riotaprop  6007  acexmidlemcase  6023  caovlem2d  6225  f1ocnvd  6235  caofcom  6275  resfunexgALT  6279  elxp7  6342  2ndrn  6355  1stconst  6395  2ndconst  6396  cnvf1olem  6398  poxp  6406  ressuppss  6432  funsssuppss  6436  dftpos4  6472  dfsmo2  6496  tfrlem5  6523  tfrlemiex  6540  tfr1onlemsucaccv  6550  tfr1onlembfn  6553  tfr1onlemex  6556  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllembfn  6566  tfrcllemex  6569  tfrcllemres  6571  tfrcl  6573  frecabex  6607  frecabcl  6608  frecfcllem  6613  frecrdg  6617  oawordi  6680  nntri3  6708  nntr2  6714  nnmordi  6727  iserd  6771  relelec  6787  erth  6791  qliftfun  6829  mapsncnv  6907  mptelixpg  6946  bren  6960  pw2f1odclem  7063  findcard2d  7123  findcard2sd  7124  isinfinf  7129  tridc  7132  nnwetri  7151  undifdcss  7158  fiintim  7166  fisseneq  7170  fidcenumlemim  7194  sbthlemi9  7207  supisolem  7250  ordiso2  7277  updjud  7324  difinfsn  7342  ctssdccl  7353  nnnninfeq  7370  omniwomnimkv  7409  pr2cv  7445  acfun  7465  exmidontriimlem2  7480  onntri45  7502  dftap2  7513  netap  7516  2omotaplemap  7519  ccfunen  7526  cc4f  7531  cc4n  7533  elni2  7577  dfplpq2  7617  dfmpq2  7618  enqbreq2  7620  enqdc1  7625  addcmpblnq  7630  addclnq  7638  nqpi  7641  addassnqg  7645  mulassnqg  7647  mulcanenq  7648  distrnqg  7650  1qec  7651  recexnq  7653  subhalfnqq  7677  enq0tr  7697  nqnq0pi  7701  nq0nn  7705  mulcanenq0ec  7708  nnnq0lem1  7709  addclnq0  7714  distrnq0  7722  addassnq0lemcl  7724  elnp1st2nd  7739  prarloc  7766  addlocprlemlt  7794  addlocprlemeq  7796  addlocprlemgt  7797  addclpr  7800  nqprm  7805  mullocprlem  7833  mullocpr  7834  mulclpr  7835  ltpopr  7858  ltaddpr  7860  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemrnd  7868  ltexprlemdisj  7869  addcanprleml  7877  addcanprlemu  7878  addcanprg  7879  recexprlemm  7887  recexprlemopl  7888  recexprlemopu  7890  recexprlemrnd  7892  recexprlemdisj  7893  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemopu  7911  cauappcvgprlemrnd  7913  cauappcvgprlemdisj  7914  cauappcvgprlemlim  7924  caucvgprlemnkj  7929  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemopu  7934  caucvgprlemrnd  7936  caucvgprlemlim  7944  caucvgprprlemnkltj  7952  caucvgprprlemnkeqj  7953  caucvgprprlemnjltk  7954  caucvgprprlemm  7959  caucvgprprlemopl  7960  caucvgprprlemopu  7962  caucvgprprlemrnd  7964  caucvgprprlemexbt  7969  caucvgprprlemlim  7974  suplocexprlemrl  7980  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemloc  7984  suplocexprlemex  7985  suplocexprlemub  7986  prsrlem1  8005  mulclsr  8017  mulasssrg  8021  distrsrg  8022  suplocsrlemb  8069  elreal2  8093  axmulass  8136  axdistr  8137  axcaucvglemcau  8161  add20  8697  mullt0  8703  rereim  8809  ltmul1  8815  cru  8825  mulap0r  8838  aprcl  8869  aptap  8873  divmuldivap  8935  divmuleqap  8940  divadddivap  8950  divmuldivapd  9055  divmuleqapd  9056  div2subap  9060  ltmul12a  9083  lemul12a  9085  lemulge11  9089  lediv12a  9117  lediv2a  9118  recgt1i  9121  recreclt  9123  ledivp1  9126  lemul1ad  9162  lemul2ad  9163  ltmul12ad  9164  lemul12ad  9165  lemul12bd  9166  nndivre  9222  nndivtr  9228  halfaddsubcl  9420  halfaddsub  9421  lt2halves  9423  nnrecl  9443  elnn0nn  9487  elnnnn0b  9489  elnnnn0c  9490  nn0addge1  9491  nn0addge2  9492  xnn0xrnemnf  9520  elnn0z  9535  elnnz1  9545  nzadd  9575  elz2  9594  zdivadd  9612  zdivmul  9613  zextle  9614  peano2uz2  9630  uzind  9634  btwnz  9642  uzss  9820  eluzp1m1  9823  infregelbex  9875  eluz2b2  9880  qre  9902  qaddcl  9912  qmulcl  9914  qreccl  9919  irradd  9923  irrmul  9924  elpqb  9927  cnref1o  9928  rprege0  9946  rprene0  9949  rpreap0  9950  rpcnne0  9951  rpcnap0  9952  rpregt0d  9981  rprege0d  9982  rprene0d  9983  rpcnne0d  9984  lediv2ad  9997  ledivge1le  10004  lediv12ad  10034  nnledivrp  10044  nn0ledivnn  10045  xrlttri3  10075  xrrebnd  10097  xrrege0  10103  xnn0xadd0  10145  xlesubadd  10161  elioo4g  10212  ioomax  10226  iccmax  10227  divelunit  10280  elfz5  10295  uzsubsubfz  10325  fzopth  10339  fzass4  10340  fzrev2  10363  uzsplit  10370  elfz2nn0  10390  difelfzle  10412  1fv  10417  4fvwrd4  10418  fzo1fzo0n0  10466  elfzom1elp1fzo  10491  subfzo0  10532  infssuzex  10537  qtri3or  10544  adddivflid  10596  flltdivnn0lt  10608  intfracq  10626  modqid2  10657  modfzo0difsn  10701  seq3val  10766  seqvalcd  10767  iseqf1olemqcl  10805  iseqf1olemnab  10807  iseqf1olemab  10808  iseqf1olemmo  10811  seq3f1olemqsumkj  10817  seq3f1olemqsumk  10818  seqf1oglem1  10825  seqf1oglem2  10826  expclzaplem  10869  leexp1a  10900  expubnd  10902  le2sq2  10921  sumsqeq0  10924  bernneq  10966  expnlbnd  10970  nn0opthd  11028  faclbnd6  11050  facavg  11052  seq3coll  11150  hash2en  11151  wrdnval  11191  ccat0  11220  ccatsymb  11226  ccatalpha  11237  swrdspsleq  11295  pfxtrcfv  11321  pfxsuffeqwrdeq  11326  wrd2ind  11351  pfxccatin12lem2a  11355  pfxccatin12  11361  pfxccat3  11362  swrdccat  11363  pfxccatpfx1  11364  pfxccatpfx2  11365  swrdccatin1d  11371  swrdccatin2d  11372  shftlem  11437  shftfvalg  11439  shftfval  11442  cvg1nlemcau  11605  cvg1nlemres  11606  rexuz3  11611  resqrexlemcvg  11640  resqrexlemglsq  11643  resqrexlemga  11644  sqrtle  11657  sqrtlt  11658  sqrt11  11660  sqrtsq2  11664  absmul  11690  sqabs  11703  abslt  11709  absle  11710  lenegsq  11716  maxleastb  11835  maxltsup  11839  rexanre  11841  negfi  11849  xrmaxiflemab  11868  xrmaxiflemlub  11869  xrmaxltsup  11879  xrmaxadd  11882  climcn2  11930  mulcn2  11933  summodclem2a  12003  summodc  12005  fsum3  12009  fsum3cvg3  12018  fsumcl2lem  12020  fsumadd  12028  fsump1i  12055  fsum0diaglem  12062  mptfzshft  12064  fsumrev  12065  fsummulc2  12070  fsum00  12084  expcnvap0  12124  mertenslemi1  12157  ntrivcvgap0  12171  prodmodclem3  12197  prodmodclem2a  12198  zproddc  12201  fprodseq  12205  fprodrev  12241  fprodconst  12242  eftlub  12312  efieq  12357  sincos1sgn  12387  demoivreALT  12396  dvdsval3  12413  dvdscmul  12440  dvdsmulc  12441  dvdscmulr  12442  dvdsmulcr  12443  modmulconst  12445  dvds2ln  12446  ltoddhalfle  12515  nn0o  12529  divalg2  12548  ndvdssub  12552  ndvdsadd  12553  divgcdz  12603  gcd0id  12611  gcdaddm  12616  bezoutlemstep  12629  bezoutlemmain  12630  dfgcd3  12642  dfgcd2  12646  lcmcllem  12700  dvdslcm  12702  lcmgcdlem  12710  lcmgcdnn  12715  qredeq  12729  qredeu  12730  rpdvds  12732  divgcdcoprm0  12734  cncongr1  12736  cncongr2  12737  cncongrcoprm  12739  prmind2  12753  isprm5  12775  isprm6  12780  prmexpb  12784  cncongrprm  12790  sqrt2irrlem  12794  pw2dvdslemn  12798  oddpwdclemxy  12802  oddpwdclemdc  12806  oddpwdc  12807  hashdvds  12854  prmdiv  12868  hashgcdlem  12871  nnoddn2prmb  12896  pythagtriplem6  12904  pythagtriplem7  12905  pcpre1  12926  pccl  12933  pcmul  12935  pcdiv  12936  pcqmul  12937  pcqcl  12940  pcdvds  12949  pcndvds  12951  pcndvds2  12953  pc2dvds  12964  dvdsprmpweqle  12971  difsqpwdvds  12972  pcaddlem  12973  pcadd  12974  pcmptcl  12976  pcmpt  12977  fldivp1  12982  pcfac  12984  oddprmdvds  12988  infpnlem2  12994  4sqlem5  13016  4sqlem6  13017  4sqlem4a  13025  4sqexercise1  13032  4sqexercise2  13033  4sqlem13m  13037  4sqlem15  13039  4sqlem16  13040  ennnfonelemfun  13099  ennnfonelemim  13106  ctinfomlemom  13109  ctinfom  13110  ctinf  13112  ctiunctlemfo  13121  omctfn  13125  fnpr2ob  13484  ismgmid2  13524  fngsum  13532  igsumvalx  13533  gsumfzval  13535  gsum0g  13540  gsumval2  13541  issgrpd  13556  ismndd  13581  prdsidlem  13591  imasmnd2  13596  mhmf1o  13614  subsubm  13627  dfgrp2  13671  isgrpid2  13684  isgrpinv  13698  grplrinv  13701  dfgrp3mlem  13742  dfgrp3m  13743  dfgrp3me  13744  prdsinvlem  13752  imasgrp2  13758  mhmmnd  13764  issubg2m  13837  issubgrpd2  13838  grpissubg  13842  subsubg  13845  subgintm  13846  isnsg3  13855  nmzsubg  13858  eqgval  13871  eqgen  13875  isghmd  13900  ghmrn  13905  ghmpreima  13914  ghmf1o  13923  conjghm  13924  conjnmzb  13928  ghmpropd  13931  rinvmod  13957  imasabl  13984  rnglz  14020  isrngd  14028  srgdilem  14044  srglmhm  14068  srgrmhm  14069  ringdilem  14087  isringd  14116  ringsrg  14122  ringinvnzdiv  14125  imasring  14139  dvdsrd  14170  unitgrp  14192  isrim0  14237  isrhm2d  14241  rhmf1o  14244  rhmco  14250  rhmopp  14252  issubrng2  14286  subsubrng  14290  subrgugrp  14316  issubrg2  14317  subsubrg  14321  resrhm  14324  aprap  14362  lmodfopnelem2  14401  lsssubg  14453  islss3  14455  islss4  14458  lspsnel6  14484  lidlacl  14560  lidlsubg  14562  lidlrsppropdg  14571  2idlelbas  14592  cnfld1  14648  cnsubglem  14655  mulgghm2  14684  zndvds  14725  psrbagcon  14752  mplsubgfi  14782  topgele  14820  tgcl  14855  epttop  14881  opnssneib  14947  iscnp4  15009  cnco  15012  cncnp  15021  cnrest2  15027  lmss  15037  txcnp  15062  txcn  15066  cnmpt12  15078  cnmpt22  15085  hmeof1o  15100  psmetres2  15124  distspace  15126  ismeti  15137  isxmetd  15138  xmetpsmet  15160  xblss2ps  15195  xblss2  15196  blcntrps  15206  blcntr  15207  blin2  15223  mopni3  15275  metequiv2  15287  bdmet  15293  xmettx  15301  cnbl0  15325  cnblcld  15326  tgioo  15345  elcncf1di  15370  dedekindeulemlu  15412  suplociccex  15416  dedekindicclemlu  15421  dedekindicc  15424  ivthinclemlopn  15427  ivthdec  15435  ivthreinc  15436  ivthdichlem  15442  cnplimcim  15458  limccnp2lem  15467  dvfvalap  15472  plymullem  15541  reeff1olem  15562  sin0pilem1  15572  pilem3  15574  ptolemy  15615  sincosq1sgn  15617  sinq12gt0  15621  ioocosf1o  15645  rprelogbmulexp  15747  perfectlem2  15791  lgslem3  15798  lgsne0  15834  gausslemma2dlem0b  15846  gausslemma2dlem0c  15847  lgsquadlem2  15874  lgsquad2lem2  15878  2lgsoddprmlem2  15902  2sqlem8  15919  gropd  15965  grstructd2dom  15966  incistruhgr  16008  umgrislfupgrenlem  16048  umgrislfupgrdom  16049  uspgrupgrushgr  16100  usgrumgruspgr  16103  usgruspgrben  16104  usgrislfuspgrdom  16108  umgrvad2edg  16129  umgr2edgneu  16130  ushgredgedg  16144  ushgredgedgloop  16146  subgrprop3  16180  iswlkg  16247  wlk2f  16269  upgriswlkdc  16278  wlkv0  16287  wlklenvclwlk  16291  wlkepvtx  16293  upgr2wlkdc  16295  wlkres  16297  clwwlkccatlem  16318  clwwlkccat  16319  clwwlknbp  16333  clwwlknp  16335  clwwlkext2edg  16340  clwwlknon  16347  clwwlknonccat  16351  clwwlknonex2  16357  clwwlknonex2e  16358  trlsegvdeglem1  16378  bj-nnan  16431  bj-charfun  16500  bdop  16568  bdunexb  16613  bj-om  16630  findset  16638  bj-peano4  16648  bj-inf2vn  16667  bj-inf2vn2  16668  pwle2  16697  pwf1oexmid  16698  nnnninfex  16725  sbthom  16731  qdencn  16732  trilpolemlt1  16750  gfsumval  16786  gfsump1  16792