MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantrr Structured version   Visualization version   GIF version

Theorem adantrr 748
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
adantrr ((𝜑 ∧ (𝜓𝜃)) → 𝜒)

Proof of Theorem adantrr
StepHypRef Expression
1 simpl 471 . 2 ((𝜓𝜃) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 489 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195  df-an 384
This theorem is referenced by:  ad2ant2r  778  ad2ant2lr  779  consensus  989  cases2  1004  3ad2antr1  1218  reusv2lem3  4791  otsndisj  4894  otiunsndisj  4895  po2nr  4961  sotric  4974  sotrieq  4975  tz7.7  5651  fmptsnd  6317  fvtp1g  6345  fsnex  6415  isocnv  6457  isores2  6460  isomin  6464  isoini  6465  f1oiso2  6479  ovmpt2df  6667  offval  6779  ordsucun  6894  xp1st  7066  1stconst  7129  cnvf1olem  7139  fnse  7158  mpt2xopoveq  7209  wfrlem3  7280  oalim  7476  omlim  7477  oaass  7505  omordi  7510  omwordri  7516  odi  7523  oen0  7530  oewordri  7536  nnawordi  7565  nnmordi  7575  omabs  7591  erinxp  7685  dom2lem  7858  mapen  7986  ssenen  7996  ssfi  8042  domfi  8043  domunfican  8095  mapfien  8173  ordtypelem6  8288  ordtypelem7  8289  card2inf  8320  inf3lem6  8390  cantnfle  8428  cantnflem1b  8443  cantnflem1  8446  wemapwe  8454  rankxplim3  8604  fseqenlem2  8708  dfac5lem4  8809  dfac2  8813  cfsuc  8939  cfflb  8941  cofsmo  8951  infpssrlem4  8988  fin4en1  8991  ssfin4  8992  fin23lem26  9007  fin23lem22  9009  fin23lem27  9010  isf34lem4  9059  isf34lem5  9060  fin1a2lem12  9093  axdc3lem2  9133  axdc4lem  9137  ttukeylem6  9196  iundom2g  9218  pwcfsdom  9261  gchen2  9304  gchor  9305  fpwwe2lem7  9314  fpwwe2lem9  9316  fpwwe2lem11  9318  fpwwe2lem12  9319  fpwwe2  9321  pwfseqlem4  9340  gchina  9377  ltexprlem6  9719  prlem936  9725  mul4  10056  2addsub  10146  muladd  10313  ltleadd  10362  leord1  10406  eqord1  10407  ltord2  10408  leord2  10409  eqord2  10410  divmul3  10541  divcan7  10585  divadddiv  10591  lemul2a  10729  lemul12b  10731  ltmuldiv2  10748  ltdivmul  10749  ledivmul  10750  ltdivmul2  10751  lt2mul2div  10752  ledivmul2  10753  lemuldiv2  10755  lt2msq  10759  ltdiv23  10765  lediv23  10766  supadd  10840  supmullem1  10842  cju  10865  zextlt  11285  suprzcl  11291  zmax  11619  xrlttr  11810  xrre3  11837  qbtwnre  11865  xrsupsslem  11967  xrinfmsslem  11968  supxrunb1  11979  supxrunb2  11980  ixxdisj  12019  iooshf  12081  icodisj  12126  iccf1o  12145  modid  12514  modadd1  12526  modmul1  12542  seqf1o  12661  expsub  12727  sqlecan  12790  bcval5  12924  hashmap  13036  hashfacen  13049  seqcoll  13059  swrdswrdlem  13259  cshwidxmod  13348  2cshwcshw  13370  cshwcshid  13372  resqreu  13789  lenegsq  13856  limsupbnd2  14010  icco1  14067  rlimresb  14092  rlimsqzlem  14175  rlimsqz  14176  rlimsqz2  14177  caucvgrlem  14199  fsum0diag2  14305  o1fsum  14334  ruclem8  14753  dvdsmulcr  14797  ndvdsadd  14920  bitsshft  14983  lcmdvds  15107  hashdvds  15266  eulerthlem2  15273  phisum  15281  pcqmul  15344  pcmpt  15382  prmreclem3  15408  4sqlem11  15445  0ram  15510  ramub1  15518  invfun  16195  initoeu2lem2  16436  coaval  16489  catcisolem  16527  funcestrcsetclem8  16558  fullestrcsetc  16562  embedsetcestrclem  16568  funcsetcestrclem8  16573  fullsetcestrc  16577  prfcl  16614  prf1st  16615  prf2nd  16616  1st2ndprf  16617  curfuncf  16649  isposd  16726  lubun  16894  isacs3lem  16937  pslem  16977  psss  16985  pwsdiagmhm  17140  gsumccat  17149  grpinvid1  17241  grpinvid2  17242  grplcan  17248  grpnpncan0  17282  dfgrp3lem  17284  dfgrp3  17285  grplactcnv  17289  0nsg  17410  eqger  17415  resghm  17447  conjghm  17462  subgga  17504  gaorber  17512  gastacl  17513  orbsta  17517  symgextf1lem  17611  psgnunilem2  17686  odid  17728  odmulg  17744  gexid  17767  odcau  17790  lsmssv  17829  lsmcom2  17841  pj1ghm  17887  frgpuptf  17954  frgpup1  17959  ghmplusg  18020  cyggex2  18069  gsumval3eu  18076  gsumval3  18079  ablfac1eu  18243  pgpfac1lem5  18249  isdrngd  18543  issrngd  18632  lmhmf1o  18815  lmhmima  18816  lmhmpreima  18817  lspextmo  18825  pwssplit2  18829  pwssplit3  18830  lspdisj  18894  islbs3  18924  lbsextlem4  18930  drngnidl  18998  lidldvgen  19024  issubassa2  19114  psrbagconf1o  19143  evlslem2  19281  ply1sclf1  19428  cnsubrg  19573  znunit  19678  cygznlem3  19684  dsmmsubg  19853  dsmmlss  19854  frlmsslsp  19901  frlmup1  19903  lindfrn  19926  f1lindf  19927  mamuass  19974  dmatmul  20069  dmatsubcl  20070  dmatmulcl  20072  dmatcrng  20074  scmataddcl  20088  scmatsubcl  20089  scmatcrng  20093  mdetunilem2  20185  pm2mpf1  20370  pm2mpghm  20387  eltg2  20520  ntrss  20616  opncldf1  20645  ssnei2  20677  neindisj  20678  restopnb  20736  restntr  20743  tgcmp  20961  hauscmplem  20966  2ndc1stc  21011  2ndcdisj  21016  2ndcomap  21018  restlly  21043  lly1stc  21056  isref  21069  islocfin  21077  comppfsc  21092  txcls  21164  txdis1cn  21195  pthaus  21198  txlm  21208  qtoptop2  21259  qtopomap  21278  kqt0lem  21296  pt1hmeo  21366  ptuncnv  21367  xkocnv  21374  fbasfip  21429  fgabs  21440  fbasrn  21445  elfm2  21509  fmfnfmlem2  21516  fmfnfmlem4  21518  ptcmplem3  21615  ptcmplem4  21616  tsmsres  21704  tsmsxplem1  21713  utoptop  21795  elbl2ps  21951  elbl2  21952  blin  21983  xmeter  21995  xmetresbl  21999  stdbdxmet  22077  metrest  22086  metustexhalf  22118  dscmet  22134  nrmmetd  22136  tngngp2  22213  nmoi2  22291  icccmplem2  22381  reconnlem2  22385  metdstri  22409  metdsle  22410  metdsre  22411  metnrmlem3  22419  fsumcn  22428  icccvx  22504  bndth  22512  evth  22513  reparphti  22552  pi1blem  22594  tchcph  22788  iscfil2  22816  cfilfcls  22824  iscau4  22829  iscauf  22830  caucfil  22833  cncmet  22871  minveclem7  22958  ovoliunlem1  23021  ovolicc2lem2  23037  ovolicc2lem3  23038  ovolicc2lem4  23039  ovolicc2lem5  23040  ovolicc2  23041  voliunlem3  23071  voliun  23073  ioombl  23084  volivth  23125  ismbfd  23157  ismbf3d  23171  itg1addlem1  23209  i1fadd  23212  itg1addlem4  23216  itg2seq  23259  itg2split  23266  itg2monolem1  23267  itg2gt0  23277  ibllem  23281  itgvallem3  23302  iblposlem  23308  dvmptfsum  23486  rolle  23501  dvlip  23504  c1liplem1  23507  lhop1  23525  lhop2  23526  dvcvx  23531  dvfsumge  23533  dvfsumrlimge0  23541  dvfsumrlim  23542  dvfsum2  23545  mdegaddle  23582  mdegvscale  23583  mdegmullem  23586  ply1divex  23644  coeeulem  23728  plyco  23745  dgrlt  23770  vieta1  23815  ulmss  23899  ulmdvlem3  23904  iblulm  23909  tanord  24032  eff1olem  24042  logdivlt  24115  logccv  24153  lawcos  24290  leibpilem1  24411  xrlimcnp  24439  cxp2limlem  24446  cxp2lim  24447  cxploglim2  24449  divsqrtsumo1  24454  lgambdd  24507  ftalem2  24544  sqff1o  24652  dvdsppwf1o  24656  dvdsflf1o  24657  musum  24661  muinv  24663  fsumdvdsmul  24665  sgmmul  24670  fsumvma  24682  logfac2  24686  chpchtsum  24688  logfacrlim  24693  logexprlim  24694  dchrelbas3  24707  dchrmulcl  24718  bposlem1  24753  lgsdchr  24824  lgsquadlem1  24849  lgsquadlem2  24850  lgsquad2lem2  24854  chebbnd1lem1  24902  chpchtlim  24912  rplogsumlem2  24918  dchrmusum2  24927  dchrvmasumlem1  24928  dchrvmasum2lem  24929  dchrvmasumlem2  24931  dchrvmasumlem3  24932  dchrvmasumiflem2  24935  dchrisum0flb  24943  dchrisum0fno1  24944  rpvmasum2  24945  dchrisum0re  24946  dchrisum0lem1  24949  dchrisum0lem2a  24950  dchrisum0lem2  24951  dchrisum0lem3  24952  rplogsum  24960  mulogsum  24965  mulog2sumlem2  24968  vmalogdivsum2  24971  2vmadivsumlem  24973  selberglem2  24979  selberg3lem1  24990  selberg4lem1  24993  selberg4  24994  pntrsumo1  24998  selberg34r  25004  pntrlog2bndlem1  25010  pntrlog2bndlem2  25011  pntrlog2bndlem3  25012  pntrlog2bndlem4  25013  pntrlog2bndlem5  25014  pntrlog2bndlem6  25016  pntibndlem3  25025  pntlemp  25043  ostthlem1  25060  ostth3  25071  ercgrg  25157  ishpg  25396  axlowdimlem15  25581  axlowdimlem16  25582  axcontlem10  25598  usgrasscusgra  25804  usgra2adedgspth  25934  usgra2adedgwlk  25935  usgra2adedgwlkon  25936  wwlknext  26045  wwlkextwrd  26049  wwlknndef  26058  clwwlknndef  26094  clwlkisclwwlklem2a  26106  frgranbnb  26340  numclwlk1lem2f1  26414  grpoidinv  26539  grporcan  26549  grpoinvid1  26559  grpoinvid2  26560  grpolcan  26561  ablo4  26581  nvabs  26704  sspph  26887  minvecolem7  26916  htthlem  26951  hvadd4  27070  hvaddsub4  27112  shscli  27353  pjspansn  27613  fh1  27654  fh2  27655  cm2j  27656  chscllem2  27674  spansncvi  27688  5oalem2  27691  5oalem5  27694  5oalem6  27695  3oalem2  27699  hoadd4  27820  cnvunop  27954  bralnfn  27984  eighmorth  28000  hmops  28056  hmopm  28057  adjlnop  28122  adjmul  28128  adjadd  28129  nmopcoi  28131  kbass5  28156  kbass6  28157  hstle  28266  stlesi  28277  mdsl0  28346  mdexchi  28371  atom1d  28389  superpos  28390  cvexchlem  28404  atomli  28418  atcvatlem  28421  chirredlem2  28427  chirredlem3  28428  atcvat4i  28433  mdsymlem1  28439  mdsymlem3  28441  mdsymlem5  28443  mdsymlem6  28444  sumdmdlem  28454  sumdmdlem2  28455  cdj1i  28469  opeldifid  28587  isoun  28655  1stpreimas  28659  f1od2  28680  archirngz  28867  archiabllem1  28871  archiabllem2c  28873  rngurd  28912  indf1ofs  29208  esum2d  29275  cntmeas  29409  ddemeas  29419  carsgclctunlem1  29499  itgeq12dv  29508  eulerpartlemgc  29544  eulerpartlemb  29550  eulerpartlemgs2  29562  ballotlemfc0  29674  ballotlemfcc  29675  signstfvneq0  29768  bnj607  30033  derangenlem  30200  subfacp1lem3  30211  subfacp1lem5  30213  cvmliftmolem2  30311  cvmliftlem6  30319  cvmlift2lem5  30336  cvmlift2lem7  30338  cvmlift2lem9  30340  mppspstlem  30515  dfon2lem6  30730  sltres  30854  colinbtwnle  31188  finminlem  31275  nn0prpwlem  31280  isfne  31297  neibastop1  31317  neibastop2lem  31318  neibastop3  31320  tailfb  31335  onsuct0  31403  nndivsub  31419  knoppcnlem6  31451  knoppndvlem9  31474  knoppndvlem18  31483  knoppndvlem21  31486  bj-finsumval0  32107  rdgeqoa  32177  matunitlindflem2  32359  poimirlem4  32366  poimirlem11  32373  poimirlem12  32374  poimirlem13  32375  poimirlem25  32387  poimirlem28  32390  heicant  32397  mblfinlem2  32400  mblfinlem3  32401  mblfinlem4  32402  mbfposadd  32410  itg2addnclem3  32416  bddiblnc  32433  ftc1anclem5  32442  ftc1anclem6  32443  ftc1anclem7  32444  ftc1anc  32446  frinfm  32483  filbcmb  32488  seqpo  32496  sstotbnd2  32526  isbndx  32534  ssbnd  32540  prdsbnd  32545  ismtycnv  32554  ismtyres  32560  heiborlem3  32565  heibor  32573  ghomdiv  32644  grpokerinj  32645  isdrngo2  32710  rngohomco  32726  rngoisocnv  32733  rngoisoco  32734  crngm4  32755  crngohomfo  32758  isidlc  32767  ispridl2  32790  ispridlc  32822  prtlem16  32955  ax12eq  33027  ax12el  33028  lshpcmp  33076  omllaw3  33333  omlfh1N  33346  cvratlem  33508  cvrat3  33529  cvrat4  33530  ps-2  33565  elpaddn0  33887  paddasslem10  33916  cdleme0cp  34302  cdleme32a  34530  cdlemeg49lebilem  34628  cdleme50eq  34630  tendoeq2  34863  diaglbN  35145  diameetN  35146  diainN  35147  dvhopN  35206  djaclN  35226  djajN  35227  dihopelvalcpre  35338  dih1dimatlem  35419  dihmeetcl  35435  djhcl  35490  mapdpglem2  35763  ismrc  36065  eldioph2  36126  lzenom  36134  rexrabdioph  36159  fphpdo  36182  irrapxlem3  36189  elpell14qr2  36227  pell14qrreccl  36229  pell14qrdich  36234  pellfundglb  36250  monotoddzzfi  36308  2nn0ind  36311  jm2.21  36362  jm2.22  36363  dnnumch3  36418  dnwech  36419  fnwe2lem2  36422  hbtlem6  36501  imo72b2lem1  37276  cncmpmax  37997  disjf1  38147  eliccelioc  38377  fprodexp  38444  fprodabs2  38445  mullimc  38466  mullimcf  38473  islpcn  38489  cncfshift  38542  cncfperiod  38547  fprodcncf  38570  dvnprodlem1  38619  dvnprodlem2  38620  stoweidlem34  38710  stoweidlem48  38724  stoweidlem60  38736  fourierdlem42  38825  fourierdlem60  38842  fourierdlem61  38843  fourierdlem63  38845  fourierdlem65  38847  fourierdlem87  38869  fourierdlem97  38879  elaa2  38910  etransclem46  38956  etransc  38959  sge0iunmptlemfi  39089  isomennd  39204  ovnsslelem  39233  ovolval4lem2  39323  ovolval5lem3  39327  smflimlem3  39442  smflimlem4  39443  smflimlem6  39445  smfpimbor1lem1  39466  icceuelpart  39758  fmtnoprmfac2  39801  bgoldbtbndlem2  40006  bgoldbtbndlem3  40007  f1cofveqaeqALT  40119  cusgrfilem1  40652  crctcsh1wlkn0  41005  wwlksnextwrd  41084  clwlkclwwlklem2a  41188  srhmsubc  41849  srhmsubcALTV  41868  aacllem  42298
  Copyright terms: Public domain W3C validator