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

Theorem adantrr 752
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 473 . 2 ((𝜓𝜃) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 491 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  ad2ant2r  782  ad2ant2lr  783  cases2  992  consensus  998  3ad2antr1  1224  reusv2lem3  4841  otsndisj  4949  otiunsndisj  4950  po2nr  5018  sotric  5031  sotrieq  5032  tz7.7  5718  fmptsnd  6400  fvtp1g  6428  f1cofveqaeqALT  6481  fsnex  6503  isocnv  6545  isores2  6548  isomin  6552  isoini  6553  f1oiso2  6567  ovmpt2df  6757  offval  6869  ordsucun  6987  xp1st  7158  1stconst  7225  cnvf1olem  7235  fnse  7254  mpt2xopoveq  7305  wfrlem3  7376  oalim  7572  omlim  7573  oaass  7601  omordi  7606  omwordri  7612  odi  7619  oen0  7626  oewordri  7632  nnawordi  7661  nnmordi  7671  omabs  7687  erinxp  7781  dom2lem  7955  mapen  8084  ssenen  8094  ssfi  8140  domfi  8141  domunfican  8193  mapfien  8273  ordtypelem6  8388  ordtypelem7  8389  card2inf  8420  inf3lem6  8490  cantnfle  8528  cantnflem1b  8543  cantnflem1  8546  wemapwe  8554  rankxplim3  8704  fseqenlem2  8808  dfac5lem4  8909  dfac2  8913  cfsuc  9039  cfflb  9041  cofsmo  9051  infpssrlem4  9088  fin4en1  9091  ssfin4  9092  fin23lem26  9107  fin23lem22  9109  fin23lem27  9110  isf34lem4  9159  isf34lem5  9160  fin1a2lem12  9193  axdc3lem2  9233  axdc4lem  9237  ttukeylem6  9296  iundom2g  9322  pwcfsdom  9365  gchen2  9408  gchor  9409  fpwwe2lem7  9418  fpwwe2lem9  9420  fpwwe2lem11  9422  fpwwe2lem12  9423  fpwwe2  9425  pwfseqlem4  9444  gchina  9481  ltexprlem6  9823  prlem936  9829  mul4  10165  2addsub  10255  muladd  10422  ltleadd  10471  leord1  10515  eqord1  10516  ltord2  10517  leord2  10518  eqord2  10519  divmul3  10650  divcan7  10694  divadddiv  10700  lemul2a  10838  lemul12b  10840  ltmuldiv2  10857  ltdivmul  10858  ledivmul  10859  ltdivmul2  10860  lt2mul2div  10861  ledivmul2  10862  lemuldiv2  10864  lt2msq  10868  ltdiv23  10874  lediv23  10875  supadd  10951  supmullem1  10953  cju  10976  zextlt  11411  suprzcl  11417  zmax  11745  xrlttr  11933  xrre3  11961  qbtwnre  11989  xrsupsslem  12096  xrinfmsslem  12097  supxrunb1  12108  supxrunb2  12109  ixxdisj  12148  iooshf  12210  icodisj  12255  iccf1o  12274  modid  12651  modadd1  12663  modmul1  12679  seqf1o  12798  expsub  12864  sqlecan  12927  bcval5  13061  hashmap  13178  hashfacen  13192  seqcoll  13202  swrdswrdlem  13413  cshwidxmod  13502  2cshwcshw  13524  cshwcshid  13526  resqreu  13943  lenegsq  14010  limsupbnd2  14164  icco1  14221  rlimresb  14246  rlimsqzlem  14329  rlimsqz  14330  rlimsqz2  14331  caucvgrlem  14353  fsum0diag2  14462  o1fsum  14491  ruclem8  14910  dvdsmulcr  14954  ndvdsadd  15077  bitsshft  15140  lcmdvds  15264  hashdvds  15423  eulerthlem2  15430  phisum  15438  pcqmul  15501  pcmpt  15539  prmreclem3  15565  4sqlem11  15602  0ram  15667  ramub1  15675  invfun  16364  initoeu2lem2  16605  coaval  16658  catcisolem  16696  funcestrcsetclem8  16727  fullestrcsetc  16731  embedsetcestrclem  16737  funcsetcestrclem8  16742  fullsetcestrc  16746  prfcl  16783  prf1st  16784  prf2nd  16785  1st2ndprf  16786  curfuncf  16818  isposd  16895  lubun  17063  isacs3lem  17106  pslem  17146  psss  17154  pwsdiagmhm  17309  gsumccat  17318  grpinvid1  17410  grpinvid2  17411  grplcan  17417  grpnpncan0  17451  dfgrp3lem  17453  dfgrp3  17454  grplactcnv  17458  0nsg  17579  eqger  17584  resghm  17616  conjghm  17631  subgga  17673  gaorber  17681  gastacl  17682  orbsta  17686  symgextf1lem  17780  psgnunilem2  17855  odid  17897  odmulg  17913  gexid  17936  odcau  17959  lsmssv  17998  lsmcom2  18010  pj1ghm  18056  frgpuptf  18123  frgpup1  18128  ghmplusg  18189  cyggex2  18238  gsumval3eu  18245  gsumval3  18248  ablfac1eu  18412  pgpfac1lem5  18418  isdrngd  18712  issrngd  18801  lmhmf1o  18986  lmhmima  18987  lmhmpreima  18988  lspextmo  18996  pwssplit2  19000  pwssplit3  19001  lspdisj  19065  islbs3  19095  lbsextlem4  19101  drngnidl  19169  lidldvgen  19195  issubassa2  19285  psrbagconf1o  19314  evlslem2  19452  ply1sclf1  19599  cnsubrg  19746  znunit  19852  cygznlem3  19858  dsmmsubg  20027  dsmmlss  20028  frlmsslsp  20075  frlmup1  20077  lindfrn  20100  f1lindf  20101  mamuass  20148  dmatmul  20243  dmatsubcl  20244  dmatmulcl  20246  dmatcrng  20248  scmataddcl  20262  scmatsubcl  20263  scmatcrng  20267  mdetunilem2  20359  pm2mpf1  20544  pm2mpghm  20561  eltg2  20702  ntrss  20799  opncldf1  20828  ssnei2  20860  neindisj  20861  restopnb  20919  restntr  20926  tgcmp  21144  hauscmplem  21149  2ndc1stc  21194  2ndcdisj  21199  2ndcomap  21201  restlly  21226  lly1stc  21239  isref  21252  islocfin  21260  comppfsc  21275  txcls  21347  txdis1cn  21378  pthaus  21381  txlm  21391  qtoptop2  21442  qtopomap  21461  kqt0lem  21479  pt1hmeo  21549  ptuncnv  21550  xkocnv  21557  fbasfip  21612  fgabs  21623  fbasrn  21628  elfm2  21692  fmfnfmlem2  21699  fmfnfmlem4  21701  ptcmplem3  21798  ptcmplem4  21799  tsmsres  21887  tsmsxplem1  21896  utoptop  21978  elbl2ps  22134  elbl2  22135  blin  22166  xmeter  22178  xmetresbl  22182  stdbdxmet  22260  metrest  22269  metustexhalf  22301  dscmet  22317  nrmmetd  22319  tngngp2  22396  nmoi2  22474  icccmplem2  22566  reconnlem2  22570  metdstri  22594  metdsle  22595  metdsre  22596  metnrmlem3  22604  fsumcn  22613  icccvx  22689  bndth  22697  evth  22698  reparphti  22737  pi1blem  22779  tchcph  22976  iscfil2  23004  cfilfcls  23012  iscau4  23017  iscauf  23018  caucfil  23021  cncmet  23059  minveclem7  23146  ovoliunlem1  23210  ovolicc2lem2  23226  ovolicc2lem3  23227  ovolicc2lem4  23228  ovolicc2lem5  23229  ovolicc2  23230  voliunlem3  23260  voliun  23262  ioombl  23273  volivth  23315  ismbfd  23347  ismbf3d  23361  itg1addlem1  23399  i1fadd  23402  itg1addlem4  23406  itg2seq  23449  itg2split  23456  itg2monolem1  23457  itg2gt0  23467  ibllem  23471  itgvallem3  23492  iblposlem  23498  dvmptfsum  23676  rolle  23691  dvlip  23694  c1liplem1  23697  lhop1  23715  lhop2  23716  dvcvx  23721  dvfsumge  23723  dvfsumrlimge0  23731  dvfsumrlim  23732  dvfsum2  23735  mdegaddle  23772  mdegvscale  23773  mdegmullem  23776  ply1divex  23834  coeeulem  23918  plyco  23935  dgrlt  23960  vieta1  24005  ulmss  24089  ulmdvlem3  24094  iblulm  24099  tanord  24222  eff1olem  24232  logdivlt  24305  logccv  24343  lawcos  24480  leibpilem1  24601  xrlimcnp  24629  cxp2limlem  24636  cxp2lim  24637  cxploglim2  24639  divsqrtsumo1  24644  lgambdd  24697  ftalem2  24734  sqff1o  24842  dvdsppwf1o  24846  dvdsflf1o  24847  musum  24851  muinv  24853  fsumdvdsmul  24855  sgmmul  24860  fsumvma  24872  logfac2  24876  chpchtsum  24878  logfacrlim  24883  logexprlim  24884  dchrelbas3  24897  dchrmulcl  24908  bposlem1  24943  lgsdchr  25014  lgsquadlem1  25039  lgsquadlem2  25040  lgsquad2lem2  25044  chebbnd1lem1  25092  chpchtlim  25102  rplogsumlem2  25108  dchrmusum2  25117  dchrvmasumlem1  25118  dchrvmasum2lem  25119  dchrvmasumlem2  25121  dchrvmasumlem3  25122  dchrvmasumiflem2  25125  dchrisum0flb  25133  dchrisum0fno1  25134  rpvmasum2  25135  dchrisum0re  25136  dchrisum0lem1  25139  dchrisum0lem2a  25140  dchrisum0lem2  25141  dchrisum0lem3  25142  rplogsum  25150  mulogsum  25155  mulog2sumlem2  25158  vmalogdivsum2  25161  2vmadivsumlem  25163  selberglem2  25169  selberg3lem1  25180  selberg4lem1  25183  selberg4  25184  pntrsumo1  25188  selberg34r  25194  pntrlog2bndlem1  25200  pntrlog2bndlem2  25201  pntrlog2bndlem3  25202  pntrlog2bndlem4  25203  pntrlog2bndlem5  25204  pntrlog2bndlem6  25206  pntibndlem3  25215  pntlemp  25233  ostthlem1  25250  ostth3  25261  ercgrg  25346  ishpg  25585  axlowdimlem15  25770  axlowdimlem16  25771  axcontlem10  25787  cusgrfilem1  26272  upgriswlk  26440  crctcshwlkn0  26616  wwlksnextwrd  26695  clwlkclwwlklem2a  26800  grpoidinv  27250  grporcan  27260  grpoinvid1  27270  grpoinvid2  27271  grpolcan  27272  ablo4  27292  nvabs  27415  sspph  27598  minvecolem7  27627  htthlem  27662  hvadd4  27781  hvaddsub4  27823  shscli  28064  pjspansn  28324  fh1  28365  fh2  28366  cm2j  28367  chscllem2  28385  spansncvi  28399  5oalem2  28402  5oalem5  28405  5oalem6  28406  3oalem2  28410  hoadd4  28531  cnvunop  28665  bralnfn  28695  eighmorth  28711  hmops  28767  hmopm  28768  adjlnop  28833  adjmul  28839  adjadd  28840  nmopcoi  28842  kbass5  28867  kbass6  28868  hstle  28977  stlesi  28988  mdsl0  29057  mdexchi  29082  atom1d  29100  superpos  29101  cvexchlem  29115  atomli  29129  atcvatlem  29132  chirredlem2  29138  chirredlem3  29139  atcvat4i  29144  mdsymlem1  29150  mdsymlem3  29152  mdsymlem5  29154  mdsymlem6  29155  sumdmdlem  29165  sumdmdlem2  29166  cdj1i  29180  opeldifid  29298  isoun  29363  1stpreimas  29367  f1od2  29383  archirngz  29570  archiabllem1  29574  archiabllem2c  29576  rngurd  29615  indf1ofs  29911  esum2d  29978  cntmeas  30112  ddemeas  30122  carsgclctunlem1  30202  itgeq12dv  30211  eulerpartlemgc  30247  eulerpartlemb  30253  eulerpartlemgs2  30265  ballotlemfc0  30377  ballotlemfcc  30378  signstfvneq0  30471  bnj607  30747  derangenlem  30914  subfacp1lem3  30925  subfacp1lem5  30927  cvmliftmolem2  31025  cvmliftlem6  31033  cvmlift2lem5  31050  cvmlift2lem7  31052  cvmlift2lem9  31054  mppspstlem  31229  dfon2lem6  31447  sltres  31571  nosino  31628  nosifv  31629  colinbtwnle  31920  finminlem  32007  nn0prpwlem  32012  isfne  32029  neibastop1  32049  neibastop2lem  32050  neibastop3  32052  tailfb  32067  onsuct0  32135  nndivsub  32151  knoppcnlem6  32183  knoppndvlem9  32206  knoppndvlem18  32215  knoppndvlem21  32218  bj-finsumval0  32819  rdgeqoa  32889  matunitlindflem2  33077  poimirlem4  33084  poimirlem11  33091  poimirlem12  33092  poimirlem13  33093  poimirlem25  33105  poimirlem28  33108  heicant  33115  mblfinlem2  33118  mblfinlem3  33119  mblfinlem4  33120  mbfposadd  33128  itg2addnclem3  33134  bddiblnc  33151  ftc1anclem5  33160  ftc1anclem6  33161  ftc1anclem7  33162  ftc1anc  33164  frinfm  33201  filbcmb  33206  seqpo  33214  sstotbnd2  33244  isbndx  33252  ssbnd  33258  prdsbnd  33263  ismtycnv  33272  ismtyres  33278  heiborlem3  33283  heibor  33291  ghomdiv  33362  grpokerinj  33363  isdrngo2  33428  rngohomco  33444  rngoisocnv  33451  rngoisoco  33452  crngm4  33473  crngohomfo  33476  isidlc  33485  ispridl2  33508  ispridlc  33540  prtlem16  33673  ax12eq  33745  ax12el  33746  lshpcmp  33794  omllaw3  34051  omlfh1N  34064  cvratlem  34226  cvrat3  34247  cvrat4  34248  ps-2  34283  elpaddn0  34605  paddasslem10  34634  cdleme0cp  35020  cdleme32a  35248  cdlemeg49lebilem  35346  cdleme50eq  35348  tendoeq2  35581  diaglbN  35863  diameetN  35864  diainN  35865  dvhopN  35924  djaclN  35944  djajN  35945  dihopelvalcpre  36056  dih1dimatlem  36137  dihmeetcl  36153  djhcl  36208  mapdpglem2  36481  ismrc  36783  eldioph2  36844  lzenom  36852  rexrabdioph  36877  fphpdo  36900  irrapxlem3  36907  elpell14qr2  36945  pell14qrreccl  36947  pell14qrdich  36952  pellfundglb  36968  monotoddzzfi  37026  2nn0ind  37029  jm2.21  37080  jm2.22  37081  dnnumch3  37136  dnwech  37137  fnwe2lem2  37140  hbtlem6  37219  imo72b2lem1  37992  cncmpmax  38713  disjf1  38878  eliccelioc  39193  fprodexp  39262  fprodabs2  39263  mullimc  39284  mullimcf  39291  islpcn  39307  limsuppnfdlem  39369  cncfshift  39422  cncfperiod  39427  fprodcncf  39449  dvnprodlem1  39498  dvnprodlem2  39499  stoweidlem34  39588  stoweidlem48  39602  stoweidlem60  39614  fourierdlem42  39703  fourierdlem60  39720  fourierdlem61  39721  fourierdlem63  39723  fourierdlem65  39725  fourierdlem87  39747  fourierdlem97  39757  elaa2  39788  etransclem46  39834  etransc  39837  sge0iunmptlemfi  39967  isomennd  40082  ovnsslelem  40111  ovolval4lem2  40201  ovolval5lem3  40205  smflimlem3  40318  smflimlem4  40319  smflimlem6  40321  smfpimbor1lem1  40342  smflimmpt  40353  smflimsupmpt  40372  icceuelpart  40700  fmtnoprmfac2  40808  bgoldbtbndlem2  41013  bgoldbtbndlem3  41014  srhmsubc  41394  srhmsubcALTV  41412  aacllem  41880
  Copyright terms: Public domain W3C validator