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  603  biadanid  614  ioran  754  ordi  818  stdcndc  847  stdcndcOLD  848  dfandc  886  mpbi2and  946  mpbir2and  947  pm4.82  953  pm4.83dc  954  rnlem  979  syl22anc  1251  syl112anc  1254  syl121anc  1255  syl211anc  1256  syl23anc  1257  syl32anc  1258  syl122anc  1259  syl212anc  1260  syl221anc  1261  syl222anc  1266  syl123anc  1267  syl132anc  1268  syl213anc  1269  syl231anc  1270  syl312anc  1271  syl321anc  1272  syl223anc  1276  syl232anc  1277  syl322anc  1278  syl233anc  1279  syl323anc  1280  syl332anc  1281  ecased  1362  19.26  1505  nfand  1592  19.40  1655  equsexd  1753  sbcof2  1834  sbequ8  1871  eu2  2099  eu3h  2100  eu5  2102  mooran2  2128  datisi  2165  felapton  2169  darapti  2170  dimatis  2172  fresison  2173  fesapo  2175  reximssdv  2611  r19.26  2633  r19.29af2  2647  r19.40  2661  eqvinc  2900  eqvincg  2901  elrabd  2935  reu6  2966  reu3  2967  indifdir  3433  undif3ss  3438  un00  3511  eqifdc  3612  disjpr2  3702  prel12  3820  prneimg  3823  preqsn  3824  disjiun  4049  opth  4294  0nelop  4305  euotd  4312  opelopabsb  4319  ispod  4364  elon2  4436  unexb  4502  opeluu  4510  eusvnfb  4514  suc11g  4618  nlimsucg  4627  tfi  4643  vtoclr  4736  opthprc  4739  ideqg  4842  resiexg  5018  dminss  5111  imainss  5112  ssxpbm  5132  relrelss  5223  funopg  5319  fununfun  5331  fntpg  5344  fun11uni  5358  imain  5370  funimaexglem  5371  funssxp  5460  ffdm  5461  f00  5484  dffo2  5519  fodmrnu  5523  foco  5526  fun11iun  5560  f1o00  5575  fsnd  5583  fv3  5617  dff2  5742  dff3im  5743  dffo4  5746  ffnfv  5756  ffvresb  5761  fsn2  5772  fconstfvm  5820  fnfvima  5837  fcof1o  5876  isocnv  5898  isotr  5903  riotaprop  5941  acexmidlemcase  5957  caovlem2d  6157  f1ocnvd  6166  caofcom  6207  resfunexgALT  6211  elxp7  6274  2ndrn  6287  1stconst  6325  2ndconst  6326  cnvf1olem  6328  poxp  6336  dftpos4  6367  dfsmo2  6391  tfrlem5  6418  tfrlemiex  6435  tfr1onlemsucaccv  6445  tfr1onlembfn  6448  tfr1onlemex  6451  tfr1onlemres  6453  tfrcllemsucaccv  6458  tfrcllembfn  6461  tfrcllemex  6464  tfrcllemres  6466  tfrcl  6468  frecabex  6502  frecabcl  6503  frecfcllem  6508  frecrdg  6512  oawordi  6573  nntri3  6601  nntr2  6607  nnmordi  6620  iserd  6664  relelec  6680  erth  6684  qliftfun  6722  mapsncnv  6800  mptelixpg  6839  bren  6853  pw2f1odclem  6951  findcard2d  7009  findcard2sd  7010  isinfinf  7015  tridc  7017  nnwetri  7034  undifdcss  7041  fiintim  7049  fisseneq  7052  fidcenumlemim  7075  sbthlemi9  7088  supisolem  7131  ordiso2  7158  updjud  7205  difinfsn  7223  ctssdccl  7234  nnnninfeq  7251  omniwomnimkv  7290  pr2cv  7326  acfun  7345  exmidontriimlem2  7360  onntri45  7382  dftap2  7393  netap  7396  2omotaplemap  7399  ccfunen  7406  cc4f  7411  cc4n  7413  elni2  7457  dfplpq2  7497  dfmpq2  7498  enqbreq2  7500  enqdc1  7505  addcmpblnq  7510  addclnq  7518  nqpi  7521  addassnqg  7525  mulassnqg  7527  mulcanenq  7528  distrnqg  7530  1qec  7531  recexnq  7533  subhalfnqq  7557  enq0tr  7577  nqnq0pi  7581  nq0nn  7585  mulcanenq0ec  7588  nnnq0lem1  7589  addclnq0  7594  distrnq0  7602  addassnq0lemcl  7604  elnp1st2nd  7619  prarloc  7646  addlocprlemlt  7674  addlocprlemeq  7676  addlocprlemgt  7677  addclpr  7680  nqprm  7685  mullocprlem  7713  mullocpr  7714  mulclpr  7715  ltpopr  7738  ltaddpr  7740  ltexprlemm  7743  ltexprlemopl  7744  ltexprlemopu  7746  ltexprlemrnd  7748  ltexprlemdisj  7749  addcanprleml  7757  addcanprlemu  7758  addcanprg  7759  recexprlemm  7767  recexprlemopl  7768  recexprlemopu  7770  recexprlemrnd  7772  recexprlemdisj  7773  cauappcvgprlemm  7788  cauappcvgprlemopl  7789  cauappcvgprlemopu  7791  cauappcvgprlemrnd  7793  cauappcvgprlemdisj  7794  cauappcvgprlemlim  7804  caucvgprlemnkj  7809  caucvgprlemm  7811  caucvgprlemopl  7812  caucvgprlemopu  7814  caucvgprlemrnd  7816  caucvgprlemlim  7824  caucvgprprlemnkltj  7832  caucvgprprlemnkeqj  7833  caucvgprprlemnjltk  7834  caucvgprprlemm  7839  caucvgprprlemopl  7840  caucvgprprlemopu  7842  caucvgprprlemrnd  7844  caucvgprprlemexbt  7849  caucvgprprlemlim  7854  suplocexprlemrl  7860  suplocexprlemru  7862  suplocexprlemdisj  7863  suplocexprlemloc  7864  suplocexprlemex  7865  suplocexprlemub  7866  prsrlem1  7885  mulclsr  7897  mulasssrg  7901  distrsrg  7902  suplocsrlemb  7949  elreal2  7973  axmulass  8016  axdistr  8017  axcaucvglemcau  8041  add20  8577  mullt0  8583  rereim  8689  ltmul1  8695  cru  8705  mulap0r  8718  aprcl  8749  aptap  8753  divmuldivap  8815  divmuleqap  8820  divadddivap  8830  divmuldivapd  8935  divmuleqapd  8936  div2subap  8940  ltmul12a  8963  lemul12a  8965  lemulge11  8969  lediv12a  8997  lediv2a  8998  recgt1i  9001  recreclt  9003  ledivp1  9006  lemul1ad  9042  lemul2ad  9043  ltmul12ad  9044  lemul12ad  9045  lemul12bd  9046  nndivre  9102  nndivtr  9108  halfaddsubcl  9300  halfaddsub  9301  lt2halves  9303  nnrecl  9323  elnn0nn  9367  elnnnn0b  9369  elnnnn0c  9370  nn0addge1  9371  nn0addge2  9372  xnn0xrnemnf  9400  elnn0z  9415  elnnz1  9425  nzadd  9455  elz2  9474  zdivadd  9492  zdivmul  9493  zextle  9494  peano2uz2  9510  uzind  9514  btwnz  9522  uzss  9699  eluzp1m1  9702  infregelbex  9749  eluz2b2  9754  qre  9776  qaddcl  9786  qmulcl  9788  qreccl  9793  irradd  9797  irrmul  9798  elpqb  9801  cnref1o  9802  rprege0  9820  rprene0  9823  rpreap0  9824  rpcnne0  9825  rpcnap0  9826  rpregt0d  9855  rprege0d  9856  rprene0d  9857  rpcnne0d  9858  lediv2ad  9871  ledivge1le  9878  lediv12ad  9908  nnledivrp  9918  nn0ledivnn  9919  xrlttri3  9949  xrrebnd  9971  xrrege0  9977  xnn0xadd0  10019  xlesubadd  10035  elioo4g  10086  ioomax  10100  iccmax  10101  divelunit  10154  elfz5  10169  uzsubsubfz  10199  fzopth  10213  fzass4  10214  fzrev2  10237  uzsplit  10244  elfz2nn0  10264  difelfzle  10286  1fv  10291  4fvwrd4  10292  fzo1fzo0n0  10339  elfzom1elp1fzo  10363  subfzo0  10403  infssuzex  10408  qtri3or  10415  adddivflid  10467  flltdivnn0lt  10479  intfracq  10497  modqid2  10528  modfzo0difsn  10572  seq3val  10637  seqvalcd  10638  iseqf1olemqcl  10676  iseqf1olemnab  10678  iseqf1olemab  10679  iseqf1olemmo  10682  seq3f1olemqsumkj  10688  seq3f1olemqsumk  10689  seqf1oglem1  10696  seqf1oglem2  10697  expclzaplem  10740  leexp1a  10771  expubnd  10773  le2sq2  10792  sumsqeq0  10795  bernneq  10837  expnlbnd  10841  nn0opthd  10899  faclbnd6  10921  facavg  10923  seq3coll  11019  hash2en  11020  wrdnval  11056  ccat0  11085  ccatsymb  11091  swrdspsleq  11153  pfxtrcfv  11179  pfxsuffeqwrdeq  11184  wrd2ind  11209  shftlem  11212  shftfvalg  11214  shftfval  11217  cvg1nlemcau  11380  cvg1nlemres  11381  rexuz3  11386  resqrexlemcvg  11415  resqrexlemglsq  11418  resqrexlemga  11419  sqrtle  11432  sqrtlt  11433  sqrt11  11435  sqrtsq2  11439  absmul  11465  sqabs  11478  abslt  11484  absle  11485  lenegsq  11491  maxleastb  11610  maxltsup  11614  rexanre  11616  negfi  11624  xrmaxiflemab  11643  xrmaxiflemlub  11644  xrmaxltsup  11654  xrmaxadd  11657  climcn2  11705  mulcn2  11708  summodclem2a  11777  summodc  11779  fsum3  11783  fsum3cvg3  11792  fsumcl2lem  11794  fsumadd  11802  fsump1i  11829  fsum0diaglem  11836  mptfzshft  11838  fsumrev  11839  fsummulc2  11844  fsum00  11858  expcnvap0  11898  mertenslemi1  11931  ntrivcvgap0  11945  prodmodclem3  11971  prodmodclem2a  11972  zproddc  11975  fprodseq  11979  fprodrev  12015  fprodconst  12016  eftlub  12086  efieq  12131  sincos1sgn  12161  demoivreALT  12170  dvdsval3  12187  dvdscmul  12214  dvdsmulc  12215  dvdscmulr  12216  dvdsmulcr  12217  modmulconst  12219  dvds2ln  12220  ltoddhalfle  12289  nn0o  12303  divalg2  12322  ndvdssub  12326  ndvdsadd  12327  divgcdz  12377  gcd0id  12385  gcdaddm  12390  bezoutlemstep  12403  bezoutlemmain  12404  dfgcd3  12416  dfgcd2  12420  lcmcllem  12474  dvdslcm  12476  lcmgcdlem  12484  lcmgcdnn  12489  qredeq  12503  qredeu  12504  rpdvds  12506  divgcdcoprm0  12508  cncongr1  12510  cncongr2  12511  cncongrcoprm  12513  prmind2  12527  isprm5  12549  isprm6  12554  prmexpb  12558  cncongrprm  12564  sqrt2irrlem  12568  pw2dvdslemn  12572  oddpwdclemxy  12576  oddpwdclemdc  12580  oddpwdc  12581  hashdvds  12628  prmdiv  12642  hashgcdlem  12645  nnoddn2prmb  12670  pythagtriplem6  12678  pythagtriplem7  12679  pcpre1  12700  pccl  12707  pcmul  12709  pcdiv  12710  pcqmul  12711  pcqcl  12714  pcdvds  12723  pcndvds  12725  pcndvds2  12727  pc2dvds  12738  dvdsprmpweqle  12745  difsqpwdvds  12746  pcaddlem  12747  pcadd  12748  pcmptcl  12750  pcmpt  12751  fldivp1  12756  pcfac  12758  oddprmdvds  12762  infpnlem2  12768  4sqlem5  12790  4sqlem6  12791  4sqlem4a  12799  4sqexercise1  12806  4sqexercise2  12807  4sqlem13m  12811  4sqlem15  12813  4sqlem16  12814  ennnfonelemfun  12873  ennnfonelemim  12880  ctinfomlemom  12883  ctinfom  12884  ctinf  12886  ctiunctlemfo  12895  omctfn  12899  fnpr2ob  13257  ismgmid2  13297  fngsum  13305  igsumvalx  13306  gsumfzval  13308  gsum0g  13313  gsumval2  13314  issgrpd  13329  ismndd  13354  prdsidlem  13364  imasmnd2  13369  mhmf1o  13387  subsubm  13400  dfgrp2  13444  isgrpid2  13457  isgrpinv  13471  grplrinv  13474  dfgrp3mlem  13515  dfgrp3m  13516  dfgrp3me  13517  prdsinvlem  13525  imasgrp2  13531  mhmmnd  13537  issubg2m  13610  issubgrpd2  13611  grpissubg  13615  subsubg  13618  subgintm  13619  isnsg3  13628  nmzsubg  13631  eqgval  13644  eqgen  13648  isghmd  13673  ghmrn  13678  ghmpreima  13687  ghmf1o  13696  conjghm  13697  conjnmzb  13701  ghmpropd  13704  rinvmod  13730  imasabl  13757  rnglz  13792  isrngd  13800  srgdilem  13816  srglmhm  13840  srgrmhm  13841  ringdilem  13859  isringd  13888  ringsrg  13894  ringinvnzdiv  13897  imasring  13911  dvdsrd  13941  unitgrp  13963  isrim0  14008  isrhm2d  14012  rhmf1o  14015  rhmco  14021  rhmopp  14023  issubrng2  14057  subsubrng  14061  subrgugrp  14087  issubrg2  14088  subsubrg  14092  resrhm  14095  aprap  14133  lmodfopnelem2  14172  lsssubg  14224  islss3  14226  islss4  14229  lspsnel6  14255  lidlacl  14331  lidlsubg  14333  lidlrsppropdg  14342  2idlelbas  14363  cnfld1  14419  cnsubglem  14426  mulgghm2  14455  zndvds  14496  mplsubgfi  14548  topgele  14586  tgcl  14621  epttop  14647  opnssneib  14713  iscnp4  14775  cnco  14778  cncnp  14787  cnrest2  14793  lmss  14803  txcnp  14828  txcn  14832  cnmpt12  14844  cnmpt22  14851  hmeof1o  14866  psmetres2  14890  distspace  14892  ismeti  14903  isxmetd  14904  xmetpsmet  14926  xblss2ps  14961  xblss2  14962  blcntrps  14972  blcntr  14973  blin2  14989  mopni3  15041  metequiv2  15053  bdmet  15059  xmettx  15067  cnbl0  15091  cnblcld  15092  tgioo  15111  elcncf1di  15136  dedekindeulemlu  15178  suplociccex  15182  dedekindicclemlu  15187  dedekindicc  15190  ivthinclemlopn  15193  ivthdec  15201  ivthreinc  15202  ivthdichlem  15208  cnplimcim  15224  limccnp2lem  15233  dvfvalap  15238  plymullem  15307  reeff1olem  15328  sin0pilem1  15338  pilem3  15340  ptolemy  15381  sincosq1sgn  15383  sinq12gt0  15387  ioocosf1o  15411  rprelogbmulexp  15513  perfectlem2  15557  lgslem3  15564  lgsne0  15600  gausslemma2dlem0b  15612  gausslemma2dlem0c  15613  lgsquadlem2  15640  lgsquad2lem2  15644  2lgsoddprmlem2  15668  2sqlem8  15685  gropd  15731  grstructd2dom  15732  incistruhgr  15771  umgrislfupgrenlem  15806  umgrislfupgrdom  15807  bj-nnan  15842  bj-charfun  15912  bdop  15980  bdunexb  16025  bj-om  16042  findset  16050  bj-peano4  16060  bj-inf2vn  16079  bj-inf2vn2  16080  pwle2  16107  pwf1oexmid  16108  nnnninfex  16131  sbthom  16137  qdencn  16138  trilpolemlt1  16152