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  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  3848  prneimg  3851  preqsn  3852  disjiun  4077  opth  4322  0nelop  4333  euotd  4340  opelopabsb  4347  ispod  4394  elon2  4466  unexb  4532  opeluu  4540  eusvnfb  4544  suc11g  4648  nlimsucg  4657  tfi  4673  vtoclr  4766  opthprc  4769  ideqg  4872  resiexg  5049  dminss  5142  imainss  5143  ssxpbm  5163  relrelss  5254  funopg  5351  fununfun  5363  fntpg  5376  fun11uni  5390  imain  5402  funimaexglem  5403  funssxp  5492  ffdm  5493  f00  5516  dffo2  5551  fodmrnu  5555  foco  5558  fun11iun  5592  f1o00  5607  fsnd  5615  fv3  5649  dff2  5778  dff3im  5779  dffo4  5782  ffnfv  5792  ffvresb  5797  fsn2  5808  fconstfvm  5856  fnfvima  5873  fcof1o  5912  isocnv  5934  isotr  5939  riotaprop  5979  acexmidlemcase  5995  caovlem2d  6197  f1ocnvd  6206  caofcom  6247  resfunexgALT  6251  elxp7  6314  2ndrn  6327  1stconst  6365  2ndconst  6366  cnvf1olem  6368  poxp  6376  dftpos4  6407  dfsmo2  6431  tfrlem5  6458  tfrlemiex  6475  tfr1onlemsucaccv  6485  tfr1onlembfn  6488  tfr1onlemex  6491  tfr1onlemres  6493  tfrcllemsucaccv  6498  tfrcllembfn  6501  tfrcllemex  6504  tfrcllemres  6506  tfrcl  6508  frecabex  6542  frecabcl  6543  frecfcllem  6548  frecrdg  6552  oawordi  6613  nntri3  6641  nntr2  6647  nnmordi  6660  iserd  6704  relelec  6720  erth  6724  qliftfun  6762  mapsncnv  6840  mptelixpg  6879  bren  6893  pw2f1odclem  6991  findcard2d  7049  findcard2sd  7050  isinfinf  7055  tridc  7057  nnwetri  7074  undifdcss  7081  fiintim  7089  fisseneq  7092  fidcenumlemim  7115  sbthlemi9  7128  supisolem  7171  ordiso2  7198  updjud  7245  difinfsn  7263  ctssdccl  7274  nnnninfeq  7291  omniwomnimkv  7330  pr2cv  7366  acfun  7385  exmidontriimlem2  7400  onntri45  7422  dftap2  7433  netap  7436  2omotaplemap  7439  ccfunen  7446  cc4f  7451  cc4n  7453  elni2  7497  dfplpq2  7537  dfmpq2  7538  enqbreq2  7540  enqdc1  7545  addcmpblnq  7550  addclnq  7558  nqpi  7561  addassnqg  7565  mulassnqg  7567  mulcanenq  7568  distrnqg  7570  1qec  7571  recexnq  7573  subhalfnqq  7597  enq0tr  7617  nqnq0pi  7621  nq0nn  7625  mulcanenq0ec  7628  nnnq0lem1  7629  addclnq0  7634  distrnq0  7642  addassnq0lemcl  7644  elnp1st2nd  7659  prarloc  7686  addlocprlemlt  7714  addlocprlemeq  7716  addlocprlemgt  7717  addclpr  7720  nqprm  7725  mullocprlem  7753  mullocpr  7754  mulclpr  7755  ltpopr  7778  ltaddpr  7780  ltexprlemm  7783  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemrnd  7788  ltexprlemdisj  7789  addcanprleml  7797  addcanprlemu  7798  addcanprg  7799  recexprlemm  7807  recexprlemopl  7808  recexprlemopu  7810  recexprlemrnd  7812  recexprlemdisj  7813  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemopu  7831  cauappcvgprlemrnd  7833  cauappcvgprlemdisj  7834  cauappcvgprlemlim  7844  caucvgprlemnkj  7849  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemopu  7854  caucvgprlemrnd  7856  caucvgprlemlim  7864  caucvgprprlemnkltj  7872  caucvgprprlemnkeqj  7873  caucvgprprlemnjltk  7874  caucvgprprlemm  7879  caucvgprprlemopl  7880  caucvgprprlemopu  7882  caucvgprprlemrnd  7884  caucvgprprlemexbt  7889  caucvgprprlemlim  7894  suplocexprlemrl  7900  suplocexprlemru  7902  suplocexprlemdisj  7903  suplocexprlemloc  7904  suplocexprlemex  7905  suplocexprlemub  7906  prsrlem1  7925  mulclsr  7937  mulasssrg  7941  distrsrg  7942  suplocsrlemb  7989  elreal2  8013  axmulass  8056  axdistr  8057  axcaucvglemcau  8081  add20  8617  mullt0  8623  rereim  8729  ltmul1  8735  cru  8745  mulap0r  8758  aprcl  8789  aptap  8793  divmuldivap  8855  divmuleqap  8860  divadddivap  8870  divmuldivapd  8975  divmuleqapd  8976  div2subap  8980  ltmul12a  9003  lemul12a  9005  lemulge11  9009  lediv12a  9037  lediv2a  9038  recgt1i  9041  recreclt  9043  ledivp1  9046  lemul1ad  9082  lemul2ad  9083  ltmul12ad  9084  lemul12ad  9085  lemul12bd  9086  nndivre  9142  nndivtr  9148  halfaddsubcl  9340  halfaddsub  9341  lt2halves  9343  nnrecl  9363  elnn0nn  9407  elnnnn0b  9409  elnnnn0c  9410  nn0addge1  9411  nn0addge2  9412  xnn0xrnemnf  9440  elnn0z  9455  elnnz1  9465  nzadd  9495  elz2  9514  zdivadd  9532  zdivmul  9533  zextle  9534  peano2uz2  9550  uzind  9554  btwnz  9562  uzss  9739  eluzp1m1  9742  infregelbex  9789  eluz2b2  9794  qre  9816  qaddcl  9826  qmulcl  9828  qreccl  9833  irradd  9837  irrmul  9838  elpqb  9841  cnref1o  9842  rprege0  9860  rprene0  9863  rpreap0  9864  rpcnne0  9865  rpcnap0  9866  rpregt0d  9895  rprege0d  9896  rprene0d  9897  rpcnne0d  9898  lediv2ad  9911  ledivge1le  9918  lediv12ad  9948  nnledivrp  9958  nn0ledivnn  9959  xrlttri3  9989  xrrebnd  10011  xrrege0  10017  xnn0xadd0  10059  xlesubadd  10075  elioo4g  10126  ioomax  10140  iccmax  10141  divelunit  10194  elfz5  10209  uzsubsubfz  10239  fzopth  10253  fzass4  10254  fzrev2  10277  uzsplit  10284  elfz2nn0  10304  difelfzle  10326  1fv  10331  4fvwrd4  10332  fzo1fzo0n0  10379  elfzom1elp1fzo  10403  subfzo0  10443  infssuzex  10448  qtri3or  10455  adddivflid  10507  flltdivnn0lt  10519  intfracq  10537  modqid2  10568  modfzo0difsn  10612  seq3val  10677  seqvalcd  10678  iseqf1olemqcl  10716  iseqf1olemnab  10718  iseqf1olemab  10719  iseqf1olemmo  10722  seq3f1olemqsumkj  10728  seq3f1olemqsumk  10729  seqf1oglem1  10736  seqf1oglem2  10737  expclzaplem  10780  leexp1a  10811  expubnd  10813  le2sq2  10832  sumsqeq0  10835  bernneq  10877  expnlbnd  10881  nn0opthd  10939  faclbnd6  10961  facavg  10963  seq3coll  11059  hash2en  11060  wrdnval  11097  ccat0  11126  ccatsymb  11132  swrdspsleq  11194  pfxtrcfv  11220  pfxsuffeqwrdeq  11225  wrd2ind  11250  pfxccatin12lem2a  11254  pfxccatin12  11260  pfxccat3  11261  swrdccat  11262  pfxccatpfx1  11263  pfxccatpfx2  11264  swrdccatin1d  11270  swrdccatin2d  11271  shftlem  11322  shftfvalg  11324  shftfval  11327  cvg1nlemcau  11490  cvg1nlemres  11491  rexuz3  11496  resqrexlemcvg  11525  resqrexlemglsq  11528  resqrexlemga  11529  sqrtle  11542  sqrtlt  11543  sqrt11  11545  sqrtsq2  11549  absmul  11575  sqabs  11588  abslt  11594  absle  11595  lenegsq  11601  maxleastb  11720  maxltsup  11724  rexanre  11726  negfi  11734  xrmaxiflemab  11753  xrmaxiflemlub  11754  xrmaxltsup  11764  xrmaxadd  11767  climcn2  11815  mulcn2  11818  summodclem2a  11887  summodc  11889  fsum3  11893  fsum3cvg3  11902  fsumcl2lem  11904  fsumadd  11912  fsump1i  11939  fsum0diaglem  11946  mptfzshft  11948  fsumrev  11949  fsummulc2  11954  fsum00  11968  expcnvap0  12008  mertenslemi1  12041  ntrivcvgap0  12055  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  fprodrev  12125  fprodconst  12126  eftlub  12196  efieq  12241  sincos1sgn  12271  demoivreALT  12280  dvdsval3  12297  dvdscmul  12324  dvdsmulc  12325  dvdscmulr  12326  dvdsmulcr  12327  modmulconst  12329  dvds2ln  12330  ltoddhalfle  12399  nn0o  12413  divalg2  12432  ndvdssub  12436  ndvdsadd  12437  divgcdz  12487  gcd0id  12495  gcdaddm  12500  bezoutlemstep  12513  bezoutlemmain  12514  dfgcd3  12526  dfgcd2  12530  lcmcllem  12584  dvdslcm  12586  lcmgcdlem  12594  lcmgcdnn  12599  qredeq  12613  qredeu  12614  rpdvds  12616  divgcdcoprm0  12618  cncongr1  12620  cncongr2  12621  cncongrcoprm  12623  prmind2  12637  isprm5  12659  isprm6  12664  prmexpb  12668  cncongrprm  12674  sqrt2irrlem  12678  pw2dvdslemn  12682  oddpwdclemxy  12686  oddpwdclemdc  12690  oddpwdc  12691  hashdvds  12738  prmdiv  12752  hashgcdlem  12755  nnoddn2prmb  12780  pythagtriplem6  12788  pythagtriplem7  12789  pcpre1  12810  pccl  12817  pcmul  12819  pcdiv  12820  pcqmul  12821  pcqcl  12824  pcdvds  12833  pcndvds  12835  pcndvds2  12837  pc2dvds  12848  dvdsprmpweqle  12855  difsqpwdvds  12856  pcaddlem  12857  pcadd  12858  pcmptcl  12860  pcmpt  12861  fldivp1  12866  pcfac  12868  oddprmdvds  12872  infpnlem2  12878  4sqlem5  12900  4sqlem6  12901  4sqlem4a  12909  4sqexercise1  12916  4sqexercise2  12917  4sqlem13m  12921  4sqlem15  12923  4sqlem16  12924  ennnfonelemfun  12983  ennnfonelemim  12990  ctinfomlemom  12993  ctinfom  12994  ctinf  12996  ctiunctlemfo  13005  omctfn  13009  fnpr2ob  13368  ismgmid2  13408  fngsum  13416  igsumvalx  13417  gsumfzval  13419  gsum0g  13424  gsumval2  13425  issgrpd  13440  ismndd  13465  prdsidlem  13475  imasmnd2  13480  mhmf1o  13498  subsubm  13511  dfgrp2  13555  isgrpid2  13568  isgrpinv  13582  grplrinv  13585  dfgrp3mlem  13626  dfgrp3m  13627  dfgrp3me  13628  prdsinvlem  13636  imasgrp2  13642  mhmmnd  13648  issubg2m  13721  issubgrpd2  13722  grpissubg  13726  subsubg  13729  subgintm  13730  isnsg3  13739  nmzsubg  13742  eqgval  13755  eqgen  13759  isghmd  13784  ghmrn  13789  ghmpreima  13798  ghmf1o  13807  conjghm  13808  conjnmzb  13812  ghmpropd  13815  rinvmod  13841  imasabl  13868  rnglz  13903  isrngd  13911  srgdilem  13927  srglmhm  13951  srgrmhm  13952  ringdilem  13970  isringd  13999  ringsrg  14005  ringinvnzdiv  14008  imasring  14022  dvdsrd  14052  unitgrp  14074  isrim0  14119  isrhm2d  14123  rhmf1o  14126  rhmco  14132  rhmopp  14134  issubrng2  14168  subsubrng  14172  subrgugrp  14198  issubrg2  14199  subsubrg  14203  resrhm  14206  aprap  14244  lmodfopnelem2  14283  lsssubg  14335  islss3  14337  islss4  14340  lspsnel6  14366  lidlacl  14442  lidlsubg  14444  lidlrsppropdg  14453  2idlelbas  14474  cnfld1  14530  cnsubglem  14537  mulgghm2  14566  zndvds  14607  mplsubgfi  14659  topgele  14697  tgcl  14732  epttop  14758  opnssneib  14824  iscnp4  14886  cnco  14889  cncnp  14898  cnrest2  14904  lmss  14914  txcnp  14939  txcn  14943  cnmpt12  14955  cnmpt22  14962  hmeof1o  14977  psmetres2  15001  distspace  15003  ismeti  15014  isxmetd  15015  xmetpsmet  15037  xblss2ps  15072  xblss2  15073  blcntrps  15083  blcntr  15084  blin2  15100  mopni3  15152  metequiv2  15164  bdmet  15170  xmettx  15178  cnbl0  15202  cnblcld  15203  tgioo  15222  elcncf1di  15247  dedekindeulemlu  15289  suplociccex  15293  dedekindicclemlu  15298  dedekindicc  15301  ivthinclemlopn  15304  ivthdec  15312  ivthreinc  15313  ivthdichlem  15319  cnplimcim  15335  limccnp2lem  15344  dvfvalap  15349  plymullem  15418  reeff1olem  15439  sin0pilem1  15449  pilem3  15451  ptolemy  15492  sincosq1sgn  15494  sinq12gt0  15498  ioocosf1o  15522  rprelogbmulexp  15624  perfectlem2  15668  lgslem3  15675  lgsne0  15711  gausslemma2dlem0b  15723  gausslemma2dlem0c  15724  lgsquadlem2  15751  lgsquad2lem2  15755  2lgsoddprmlem2  15779  2sqlem8  15796  gropd  15842  grstructd2dom  15843  incistruhgr  15884  umgrislfupgrenlem  15922  umgrislfupgrdom  15923  uspgrupgrushgr  15974  usgrumgruspgr  15977  usgruspgrben  15978  usgrislfuspgrdom  15982  umgrvad2edg  16003  umgr2edgneu  16004  ushgredgedg  16018  ushgredgedgloop  16020  iswlkg  16032  bj-nnan  16058  bj-charfun  16128  bdop  16196  bdunexb  16241  bj-om  16258  findset  16266  bj-peano4  16276  bj-inf2vn  16295  bj-inf2vn2  16296  pwle2  16323  pwf1oexmid  16324  nnnninfex  16347  sbthom  16353  qdencn  16354  trilpolemlt1  16368