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

Theorem adantrr 713
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 483 . 2 ((𝜓𝜃) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 592 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  ad2antrl  724  ad2ant2r  743  ad2ant2lr  744  cases2ALT  1040  consensus  1044  3adant3  1124  3ad2antr1  1180  reusv2lem3  5292  axprlem4  5318  otsndisj  5401  otiunsndisj  5402  po2nr  5481  sotric  5495  sotrieq  5496  tz7.7  6211  fmptsnd  6924  fvtp1g  6953  f1cofveqaeqALT  7008  fsnex  7030  isocnv  7072  isores2  7075  isomin  7079  isoini  7080  f1oiso2  7094  ovmpodf  7295  offval  7405  ordsucun  7528  xp1st  7712  cnvf1olem  7796  fnse  7818  mpoxopoveq  7876  wfrlem3  7947  oalim  8148  omlim  8149  oaass  8177  omordi  8182  omwordri  8188  odi  8195  oen0  8202  oewordri  8208  nnawordi  8237  nnmordi  8247  omabs  8264  erinxp  8361  dom2lem  8538  mapen  8670  ssenen  8680  ssfi  8727  domfi  8728  domunfican  8780  mapfien  8860  ordtypelem6  8976  ordtypelem7  8977  card2inf  9008  inf3lem6  9085  cantnfle  9123  cantnflem1b  9138  cantnflem1  9141  wemapwe  9149  rankxplim3  9299  fseqenlem2  9440  dfac5lem4  9541  dfac2b  9545  cfsuc  9668  cfflb  9670  cofsmo  9680  infpssrlem4  9717  fin4en1  9720  ssfin4  9721  fin23lem26  9736  fin23lem22  9738  fin23lem27  9739  isf34lem4  9788  isf34lem5  9789  fin1a2lem12  9822  axdc3lem2  9862  axdc4lem  9866  ttukeylem6  9925  iundom2g  9951  pwcfsdom  9994  gchen2  10037  gchor  10038  fpwwe2lem7  10047  fpwwe2lem9  10049  fpwwe2lem11  10051  fpwwe2lem12  10052  fpwwe2  10054  pwfseqlem4  10073  gchina  10110  ltexprlem6  10452  prlem936  10458  mul4  10797  2addsub  10889  muladd  11061  ltleadd  11112  leord1  11156  eqord1  11157  ltord2  11158  leord2  11159  eqord2  11160  divmul3  11292  divcan7  11338  divadddiv  11344  lemul2a  11484  lemul12b  11486  ltmuldiv2  11503  ltdivmul  11504  ledivmul  11505  ltdivmul2  11506  lt2mul2div  11507  ledivmul2  11508  lemuldiv2  11510  lt2msq  11514  ltdiv23  11520  lediv23  11521  fimaxre  11573  supadd  11598  supmullem1  11600  cju  11623  zextlt  12045  suprzcl  12051  zmax  12334  xrlttr  12523  xrre3  12554  qbtwnre  12582  xrsupsslem  12690  xrinfmsslem  12691  supxrunb1  12702  supxrunb2  12703  ixxdisj  12743  iooshf  12805  icodisj  12852  iccf1o  12872  modid  13254  modadd1  13266  modmul1  13282  seqf1o  13401  expsub  13467  sqlecan  13561  bcval5  13668  hashmap  13786  hashfacen  13802  seqcoll  13812  swrdswrdlem  14056  swrdccatin2  14081  cshwidxmod  14155  2cshwcshw  14177  cshwcshid  14179  resqreu  14602  lenegsq  14670  limsupbnd2  14830  icco1  14887  rlimresb  14912  rlimsqzlem  14995  rlimsqz  14996  rlimsqz2  14997  caucvgrlem  15019  fsum0diag2  15128  o1fsum  15158  ruclem8  15580  dvdsmulcr  15629  ndvdsadd  15751  bitsshft  15814  lcmdvds  15942  hashdvds  16102  eulerthlem2  16109  phisum  16117  pcqmul  16180  pcmpt  16218  prmreclem3  16244  4sqlem11  16281  0ram  16346  ramub1  16354  invfun  17024  initoeu2lem2  17265  coaval  17318  catcisolem  17356  funcestrcsetclem8  17387  fullestrcsetc  17391  embedsetcestrclem  17397  funcsetcestrclem8  17402  fullsetcestrc  17406  prfcl  17443  prf1st  17444  prf2nd  17445  1st2ndprf  17446  curfuncf  17478  isposd  17555  lubun  17723  isacs3lem  17766  pslem  17806  psss  17814  pwsdiagmhm  17985  gsumccatOLD  17995  grpinvid1  18094  grpinvid2  18095  grplcan  18101  grpnpncan0  18135  dfgrp3lem  18137  dfgrp3  18138  grplactcnv  18142  0nsg  18261  eqger  18270  resghm  18314  conjghm  18329  subgga  18370  gaorber  18378  gastacl  18379  orbsta  18383  symgextf1lem  18479  psgnunilem2  18554  odid  18597  odmulg  18614  gexid  18637  odcau  18660  lsmssv  18699  lsmcom2  18711  pj1ghm  18760  frgpuptf  18827  frgpup1  18832  ghmplusg  18897  cyggex2  18948  gsumval3eu  18955  gsumval3  18958  ablfac1eu  19126  pgpfac1lem5  19132  ablsimpgfind  19163  isdrngd  19458  issrngd  19563  lmhmf1o  19749  lmhmima  19750  lmhmpreima  19751  lspextmo  19759  pwssplit2  19763  pwssplit3  19764  lspdisj  19828  islbs3  19858  lbsextlem4  19864  drngnidl  19932  lidldvgen  19958  issubassa2  20051  psrbagconf1o  20084  evlslem2  20222  mhplss  20272  ply1sclf1  20387  cnsubrg  20535  znunit  20640  cygznlem3  20646  dsmmsubg  20817  dsmmlss  20818  frlmsslsp  20870  frlmup1  20872  lindfrn  20895  f1lindf  20896  mamuass  20941  dmatmul  21036  dmatsubcl  21037  dmatmulcl  21039  dmatcrng  21041  scmataddcl  21055  scmatsubcl  21056  scmatcrng  21060  mdetunilem2  21152  pm2mpf1  21337  pm2mpghm  21354  eltg2  21496  ntrss  21593  opncldf1  21622  ssnei2  21654  neindisj  21655  restopnb  21713  restntr  21720  tgcmp  21939  hauscmplem  21944  2ndc1stc  21989  2ndcdisj  21994  2ndcomap  21996  restlly  22021  lly1stc  22034  isref  22047  islocfin  22055  comppfsc  22070  txcls  22142  txdis1cn  22173  pthaus  22176  txlm  22186  qtoptop2  22237  qtopomap  22256  kqt0lem  22274  pt1hmeo  22344  ptuncnv  22345  xkocnv  22352  fbasfip  22406  fgabs  22417  fbasrn  22422  elfm2  22486  fmfnfmlem2  22493  fmfnfmlem4  22495  ptcmplem3  22592  ptcmplem4  22593  tsmsres  22681  tsmsxplem1  22690  utoptop  22772  elbl2ps  22928  elbl2  22929  blin  22960  xmeter  22972  xmetresbl  22976  stdbdxmet  23054  metrest  23063  metustexhalf  23095  dscmet  23111  nrmmetd  23113  tngngp2  23190  nmoi2  23268  icccmplem2  23360  reconnlem2  23364  metdstri  23388  metdsle  23389  metdsre  23390  metnrmlem3  23398  fsumcn  23407  icccvx  23483  bndth  23491  evth  23492  reparphti  23530  pi1blem  23572  tcphcph  23769  iscfil2  23798  cfilfcls  23806  iscau4  23811  iscauf  23812  caucfil  23815  cncmet  23854  minveclem7  23967  ovoliunlem1  24032  ovolicc2lem2  24048  ovolicc2lem3  24049  ovolicc2lem4  24050  ovolicc2lem5  24051  ovolicc2  24052  voliunlem3  24082  voliun  24084  ioombl  24095  volivth  24137  ismbfd  24169  ismbf3d  24184  itg1addlem1  24222  i1fadd  24225  itg1addlem4  24229  itg2split  24279  itg2monolem1  24280  itg2gt0  24290  ibllem  24294  itgvallem3  24315  iblposlem  24321  dvmptfsum  24501  rolle  24516  dvlip  24519  c1liplem1  24522  lhop1  24540  lhop2  24541  dvcvx  24546  dvfsumge  24548  dvfsumrlimge0  24556  dvfsumrlim  24557  dvfsum2  24560  mdegaddle  24597  mdegvscale  24598  mdegmullem  24601  ply1divex  24659  coeeulem  24743  plyco  24760  dgrlt  24785  vieta1  24830  ulmss  24914  ulmdvlem3  24919  iblulm  24924  tanord  25049  eff1olem  25059  logdivlt  25131  logccv  25173  lawcos  25321  leibpilem1OLD  25446  xrlimcnp  25474  cxp2limlem  25481  cxp2lim  25482  cxploglim2  25484  divsqrtsumo1  25489  lgambdd  25542  sqff1o  25687  dvdsppwf1o  25691  dvdsflf1o  25692  musum  25696  muinv  25698  fsumdvdsmul  25700  sgmmul  25705  fsumvma  25717  logfac2  25721  chpchtsum  25723  logfacrlim  25728  logexprlim  25729  dchrelbas3  25742  dchrmulcl  25753  bposlem1  25788  lgsdchr  25859  lgsquadlem1  25884  lgsquadlem2  25885  lgsquad2lem2  25889  chebbnd1lem1  25973  chpchtlim  25983  rplogsumlem2  25989  dchrmusum2  25998  dchrvmasumlem1  25999  dchrvmasum2lem  26000  dchrvmasumlem2  26002  dchrvmasumlem3  26003  dchrvmasumiflem2  26006  dchrisum0flb  26014  dchrisum0fno1  26015  rpvmasum2  26016  dchrisum0re  26017  dchrisum0lem1  26020  dchrisum0lem2a  26021  dchrisum0lem2  26022  dchrisum0lem3  26023  rplogsum  26031  mulogsum  26036  mulog2sumlem2  26039  vmalogdivsum2  26042  2vmadivsumlem  26044  selberglem2  26050  selberg3lem1  26061  selberg4lem1  26064  selberg4  26065  pntrsumo1  26069  selberg34r  26075  pntrlog2bndlem1  26081  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntibndlem3  26096  pntlemp  26114  ostthlem1  26131  ostth3  26142  ercgrg  26231  oppperpex  26467  axlowdimlem15  26670  axlowdimlem16  26671  axcontlem10  26687  cusgrfilem1  27165  upgriswlk  27350  crctcshwlkn0  27527  wwlksnext  27599  wwlksnextwrd  27603  clwlkclwwlklem2a  27704  wwlksext2clwwlk  27764  grpoidinv  28213  grporcan  28223  grpoinvid1  28233  grpoinvid2  28234  grpolcan  28235  ablo4  28255  nvabs  28377  minvecolem7  28588  htthlem  28622  hvadd4  28741  hvaddsub4  28783  shscli  29022  pjspansn  29282  fh1  29323  fh2  29324  cm2j  29325  chscllem2  29343  spansncvi  29357  5oalem2  29360  5oalem5  29363  5oalem6  29364  3oalem2  29368  hoadd4  29489  cnvunop  29623  bralnfn  29653  eighmorth  29669  hmops  29725  hmopm  29726  adjlnop  29791  adjmul  29797  adjadd  29798  nmopcoi  29800  kbass5  29825  kbass6  29826  hstle  29935  stlesi  29946  mdsl0  30015  mdexchi  30040  atom1d  30058  superpos  30059  cvexchlem  30073  atomli  30087  atcvatlem  30090  chirredlem2  30096  chirredlem3  30097  atcvat4i  30102  mdsymlem1  30108  mdsymlem3  30110  mdsymlem5  30112  mdsymlem6  30113  sumdmdlem  30123  sumdmdlem2  30124  cdj1i  30138  opeldifid  30278  isoun  30364  1stpreimas  30368  f1od2  30384  ccatf1  30553  archirngz  30746  archiabllem1  30750  archiabllem2c  30752  rngurd  30785  qusxpid  30856  indf1ofs  31185  esum2d  31252  cntmeas  31385  ddemeas  31395  carsgclctunlem1  31475  itgeq12dv  31484  eulerpartlemgc  31520  eulerpartlemb  31526  eulerpartlemgs2  31538  ballotlemfc0  31650  ballotlemfcc  31651  reprss  31788  reprpmtf1o  31797  hgt750lemb  31827  bnj607  32088  derangenlem  32316  subfacp1lem3  32327  subfacp1lem5  32329  cvmliftmolem2  32427  cvmliftlem6  32435  cvmlift2lem5  32452  cvmlift2lem7  32454  cvmlift2lem9  32456  mppspstlem  32716  dfon2lem6  32931  frrlem3  33023  frrlem13  33033  sltres  33067  noresle  33098  nosupno  33101  colinbtwnle  33477  finminlem  33564  nn0prpwlem  33568  isfne  33585  neibastop1  33605  neibastop2lem  33606  neibastop3  33608  tailfb  33623  onsuct0  33687  nndivsub  33703  knoppcnlem6  33735  knoppndvlem9  33757  knoppndvlem18  33766  knoppndvlem21  33769  bj-finsumval0  34456  rdgeqoa  34534  pibt2  34581  lindsadd  34767  matunitlindflem2  34771  poimirlem4  34778  poimirlem11  34785  poimirlem12  34786  poimirlem13  34787  poimirlem25  34799  poimirlem28  34802  heicant  34809  mblfinlem2  34812  mblfinlem3  34813  mblfinlem4  34814  mbfposadd  34821  itg2addnclem3  34827  bddiblnc  34844  ftc1anclem5  34853  ftc1anclem6  34854  ftc1anclem7  34855  ftc1anc  34857  frinfm  34893  filbcmb  34898  seqpo  34905  sstotbnd2  34935  isbndx  34943  ssbnd  34949  prdsbnd  34954  ismtycnv  34963  ismtyres  34969  heiborlem3  34974  heibor  34982  ghomdiv  35053  grpokerinj  35054  isdrngo2  35119  rngohomco  35135  rngoisocnv  35142  rngoisoco  35143  crngm4  35164  crngohomfo  35167  isidlc  35176  ispridl2  35199  ispridlc  35231  prtlem16  35887  ax12eq  35959  ax12el  35960  lshpcmp  36006  omllaw3  36263  omlfh1N  36276  cvratlem  36439  cvrat3  36460  cvrat4  36461  ps-2  36496  elpaddn0  36818  paddasslem10  36847  cdleme0cp  37232  cdleme32a  37459  cdlemeg49lebilem  37557  cdleme50eq  37559  tendoeq2  37792  diaglbN  38073  diameetN  38074  diainN  38075  dvhopN  38134  djaclN  38154  djajN  38155  dihopelvalcpre  38266  dih1dimatlem  38347  dihmeetcl  38363  djhcl  38418  mapdpglem2  38691  frlmsnic  39029  0prjspn  39150  ismrc  39178  eldioph2  39239  lzenom  39247  rexrabdioph  39271  fphpdo  39294  irrapxlem3  39301  elpell14qr2  39339  pell14qrreccl  39341  pell14qrdich  39346  pellfundglb  39362  monotoddzzfi  39419  2nn0ind  39422  jm2.21  39471  jm2.22  39472  dnnumch3  39527  dnwech  39528  fnwe2lem2  39531  hbtlem6  39609  imo72b2lem1  40402  mnuprdlem1  40488  mnuprdlem2  40489  cncmpmax  41169  disjf1  41323  eliccelioc  41677  fprodexp  41755  fprodabs2  41756  mullimc  41777  mullimcf  41784  islpcn  41800  limsuppnfdlem  41862  liminfval2  41929  xlimmnfvlem1  41993  xlimmnfvlem2  41994  xlimpnfvlem1  41997  xlimpnfvlem2  41998  cncfshift  42037  cncfperiod  42042  fprodcncf  42064  dvnprodlem1  42111  dvnprodlem2  42112  stoweidlem34  42200  stoweidlem48  42214  stoweidlem60  42226  fourierdlem42  42315  fourierdlem60  42332  fourierdlem61  42333  fourierdlem63  42335  fourierdlem65  42337  fourierdlem87  42359  fourierdlem97  42369  elaa2  42400  etransclem46  42446  etransc  42449  sge0iunmptlemfi  42576  isomennd  42694  ovnsslelem  42723  ovolval4lem2  42813  ovolval5lem3  42817  smflimlem3  42930  smflimlem4  42931  smflimlem6  42933  smfpimbor1lem1  42954  smflimmpt  42965  smflimsupmpt  42984  smfliminfmpt  42987  icceuelpart  43443  prproropf1olem4  43515  fmtnoprmfac2  43576  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  srhmsubc  44245  srhmsubcALTV  44263  aacllem  44800
  Copyright terms: Public domain W3C validator