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  8696  mullt0  8702  rereim  8808  ltmul1  8814  cru  8824  mulap0r  8837  aprcl  8868  aptap  8872  divmuldivap  8934  divmuleqap  8939  divadddivap  8949  divmuldivapd  9054  divmuleqapd  9055  div2subap  9059  ltmul12a  9082  lemul12a  9084  lemulge11  9088  lediv12a  9116  lediv2a  9117  recgt1i  9120  recreclt  9122  ledivp1  9125  lemul1ad  9161  lemul2ad  9162  ltmul12ad  9163  lemul12ad  9164  lemul12bd  9165  nndivre  9221  nndivtr  9227  halfaddsubcl  9419  halfaddsub  9420  lt2halves  9422  nnrecl  9442  elnn0nn  9486  elnnnn0b  9488  elnnnn0c  9489  nn0addge1  9490  nn0addge2  9491  xnn0xrnemnf  9521  elnn0z  9536  elnnz1  9546  nzadd  9576  elz2  9595  zdivadd  9613  zdivmul  9614  zextle  9615  peano2uz2  9631  uzind  9635  btwnz  9643  uzss  9821  eluzp1m1  9824  infregelbex  9876  eluz2b2  9881  qre  9903  qaddcl  9913  qmulcl  9915  qreccl  9920  irradd  9924  irrmul  9925  elpqb  9928  cnref1o  9929  rprege0  9947  rprene0  9950  rpreap0  9951  rpcnne0  9952  rpcnap0  9953  rpregt0d  9982  rprege0d  9983  rprene0d  9984  rpcnne0d  9985  lediv2ad  9998  ledivge1le  10005  lediv12ad  10035  nnledivrp  10045  nn0ledivnn  10046  xrlttri3  10076  xrrebnd  10098  xrrege0  10104  xnn0xadd0  10146  xlesubadd  10162  elioo4g  10213  ioomax  10227  iccmax  10228  divelunit  10281  elfz5  10297  uzsubsubfz  10327  fzopth  10341  fzass4  10342  fzrev2  10365  uzsplit  10372  elfz2nn0  10392  difelfzle  10414  1fv  10419  4fvwrd4  10420  fzo1fzo0n0  10468  elfzom1elp1fzo  10493  subfzo0  10534  infssuzex  10539  qtri3or  10546  adddivflid  10598  flltdivnn0lt  10610  intfracq  10628  modqid2  10659  modfzo0difsn  10703  seq3val  10768  seqvalcd  10769  iseqf1olemqcl  10807  iseqf1olemnab  10809  iseqf1olemab  10810  iseqf1olemmo  10813  seq3f1olemqsumkj  10819  seq3f1olemqsumk  10820  seqf1oglem1  10827  seqf1oglem2  10828  expclzaplem  10871  leexp1a  10902  expubnd  10904  le2sq2  10923  sumsqeq0  10926  bernneq  10968  expnlbnd  10972  nn0opthd  11030  faclbnd6  11052  facavg  11054  seq3coll  11152  hash2en  11153  wrdnval  11193  ccat0  11222  ccatsymb  11228  ccatalpha  11239  swrdspsleq  11297  pfxtrcfv  11323  pfxsuffeqwrdeq  11328  wrd2ind  11353  pfxccatin12lem2a  11357  pfxccatin12  11363  pfxccat3  11364  swrdccat  11365  pfxccatpfx1  11366  pfxccatpfx2  11367  swrdccatin1d  11373  swrdccatin2d  11374  shftlem  11439  shftfvalg  11441  shftfval  11444  cvg1nlemcau  11607  cvg1nlemres  11608  rexuz3  11613  resqrexlemcvg  11642  resqrexlemglsq  11645  resqrexlemga  11646  sqrtle  11659  sqrtlt  11660  sqrt11  11662  sqrtsq2  11666  absmul  11692  sqabs  11705  abslt  11711  absle  11712  lenegsq  11718  maxleastb  11837  maxltsup  11841  rexanre  11843  negfi  11851  xrmaxiflemab  11870  xrmaxiflemlub  11871  xrmaxltsup  11881  xrmaxadd  11884  climcn2  11932  mulcn2  11935  summodclem2a  12005  summodc  12007  fsum3  12011  fsum3cvg3  12020  fsumcl2lem  12022  fsumadd  12030  fsump1i  12057  fsum0diaglem  12064  mptfzshft  12066  fsumrev  12067  fsummulc2  12072  fsum00  12086  expcnvap0  12126  mertenslemi1  12159  ntrivcvgap0  12173  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  fprodrev  12243  fprodconst  12244  eftlub  12314  efieq  12359  sincos1sgn  12389  demoivreALT  12398  dvdsval3  12415  dvdscmul  12442  dvdsmulc  12443  dvdscmulr  12444  dvdsmulcr  12445  modmulconst  12447  dvds2ln  12448  ltoddhalfle  12517  nn0o  12531  divalg2  12550  ndvdssub  12554  ndvdsadd  12555  divgcdz  12605  gcd0id  12613  gcdaddm  12618  bezoutlemstep  12631  bezoutlemmain  12632  dfgcd3  12644  dfgcd2  12648  lcmcllem  12702  dvdslcm  12704  lcmgcdlem  12712  lcmgcdnn  12717  qredeq  12731  qredeu  12732  rpdvds  12734  divgcdcoprm0  12736  cncongr1  12738  cncongr2  12739  cncongrcoprm  12741  prmind2  12755  isprm5  12777  isprm6  12782  prmexpb  12786  cncongrprm  12792  sqrt2irrlem  12796  pw2dvdslemn  12800  oddpwdclemxy  12804  oddpwdclemdc  12808  oddpwdc  12809  hashdvds  12856  prmdiv  12870  hashgcdlem  12873  nnoddn2prmb  12898  pythagtriplem6  12906  pythagtriplem7  12907  pcpre1  12928  pccl  12935  pcmul  12937  pcdiv  12938  pcqmul  12939  pcqcl  12942  pcdvds  12951  pcndvds  12953  pcndvds2  12955  pc2dvds  12966  dvdsprmpweqle  12973  difsqpwdvds  12974  pcaddlem  12975  pcadd  12976  pcmptcl  12978  pcmpt  12979  fldivp1  12984  pcfac  12986  oddprmdvds  12990  infpnlem2  12996  4sqlem5  13018  4sqlem6  13019  4sqlem4a  13027  4sqexercise1  13034  4sqexercise2  13035  4sqlem13m  13039  4sqlem15  13041  4sqlem16  13042  ennnfonelemfun  13101  ennnfonelemim  13108  ctinfomlemom  13111  ctinfom  13112  ctinf  13114  ctiunctlemfo  13123  omctfn  13127  fnpr2ob  13486  ismgmid2  13526  fngsum  13534  igsumvalx  13535  gsumfzval  13537  gsum0g  13542  gsumval2  13543  issgrpd  13558  ismndd  13583  prdsidlem  13593  imasmnd2  13598  mhmf1o  13616  subsubm  13629  dfgrp2  13673  isgrpid2  13686  isgrpinv  13700  grplrinv  13703  dfgrp3mlem  13744  dfgrp3m  13745  dfgrp3me  13746  prdsinvlem  13754  imasgrp2  13760  mhmmnd  13766  issubg2m  13839  issubgrpd2  13840  grpissubg  13844  subsubg  13847  subgintm  13848  isnsg3  13857  nmzsubg  13860  eqgval  13873  eqgen  13877  isghmd  13902  ghmrn  13907  ghmpreima  13916  ghmf1o  13925  conjghm  13926  conjnmzb  13930  ghmpropd  13933  rinvmod  13959  imasabl  13986  rnglz  14022  isrngd  14030  srgdilem  14046  srglmhm  14070  srgrmhm  14071  ringdilem  14089  isringd  14118  ringsrg  14124  ringinvnzdiv  14127  imasring  14141  dvdsrd  14172  unitgrp  14194  isrim0  14239  isrhm2d  14243  rhmf1o  14246  rhmco  14252  rhmopp  14254  issubrng2  14288  subsubrng  14292  subrgugrp  14318  issubrg2  14319  subsubrg  14323  resrhm  14326  aprap  14365  lmodfopnelem2  14404  lsssubg  14456  islss3  14458  islss4  14461  lspsnel6  14487  lidlacl  14563  lidlsubg  14565  lidlrsppropdg  14574  2idlelbas  14595  cnfld1  14651  cnsubglem  14658  mulgghm2  14687  zndvds  14728  psrbagcon  14755  mplsubgfi  14785  topgele  14823  tgcl  14858  epttop  14884  opnssneib  14950  iscnp4  15012  cnco  15015  cncnp  15024  cnrest2  15030  lmss  15040  txcnp  15065  txcn  15069  cnmpt12  15081  cnmpt22  15088  hmeof1o  15103  psmetres2  15127  distspace  15129  ismeti  15140  isxmetd  15141  xmetpsmet  15163  xblss2ps  15198  xblss2  15199  blcntrps  15209  blcntr  15210  blin2  15226  mopni3  15278  metequiv2  15290  bdmet  15296  xmettx  15304  cnbl0  15328  cnblcld  15329  tgioo  15348  elcncf1di  15373  dedekindeulemlu  15415  suplociccex  15419  dedekindicclemlu  15424  dedekindicc  15427  ivthinclemlopn  15430  ivthdec  15438  ivthreinc  15439  ivthdichlem  15445  cnplimcim  15461  limccnp2lem  15470  dvfvalap  15475  plymullem  15544  reeff1olem  15565  sin0pilem1  15575  pilem3  15577  ptolemy  15618  sincosq1sgn  15620  sinq12gt0  15624  ioocosf1o  15648  rprelogbmulexp  15750  pellexlem3  15776  perfectlem2  15797  lgslem3  15804  lgsne0  15840  gausslemma2dlem0b  15852  gausslemma2dlem0c  15853  lgsquadlem2  15880  lgsquad2lem2  15884  2lgsoddprmlem2  15908  2sqlem8  15925  gropd  15971  grstructd2dom  15972  incistruhgr  16014  umgrislfupgrenlem  16054  umgrislfupgrdom  16055  uspgrupgrushgr  16106  usgrumgruspgr  16109  usgruspgrben  16110  usgrislfuspgrdom  16114  umgrvad2edg  16135  umgr2edgneu  16136  ushgredgedg  16150  ushgredgedgloop  16152  subgrprop3  16186  iswlkg  16253  wlk2f  16275  upgriswlkdc  16284  wlkv0  16293  wlklenvclwlk  16297  wlkepvtx  16299  upgr2wlkdc  16301  wlkres  16303  clwwlkccatlem  16324  clwwlkccat  16325  clwwlknbp  16339  clwwlknp  16341  clwwlkext2edg  16346  clwwlknon  16353  clwwlknonccat  16357  clwwlknonex2  16363  clwwlknonex2e  16364  trlsegvdeglem1  16384  bj-nnan  16437  bj-charfun  16506  bdop  16574  bdunexb  16619  bj-om  16636  findset  16644  bj-peano4  16654  bj-inf2vn  16673  bj-inf2vn2  16674  pwle2  16703  pwf1oexmid  16704  nnnninfex  16731  sbthom  16737  qdencn  16738  trilpolemlt1  16756  gfsumval  16792  gfsump1  16798