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

Theorem adantrr 753
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 472 . 2 ((𝜓𝜃) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 490 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  ad2ant2r  798  ad2ant2lr  799  cases2ALT  1017  consensus  1023  3ad2antr1  1246  reusv2lem3  4901  otsndisj  5008  otiunsndisj  5009  po2nr  5077  sotric  5090  sotrieq  5091  tz7.7  5787  fmptsnd  6476  fvtp1g  6504  f1cofveqaeqALT  6556  fsnex  6578  isocnv  6620  isores2  6623  isomin  6627  isoini  6628  f1oiso2  6642  ovmpt2df  6834  offval  6946  ordsucun  7067  xp1st  7242  1stconst  7310  cnvf1olem  7320  fnse  7339  mpt2xopoveq  7390  wfrlem3  7461  oalim  7657  omlim  7658  oaass  7686  omordi  7691  omwordri  7697  odi  7704  oen0  7711  oewordri  7717  nnawordi  7746  nnmordi  7756  omabs  7772  erinxp  7864  dom2lem  8037  mapen  8165  ssenen  8175  ssfi  8221  domfi  8222  domunfican  8274  mapfien  8354  ordtypelem6  8469  ordtypelem7  8470  card2inf  8501  inf3lem6  8568  cantnfle  8606  cantnflem1b  8621  cantnflem1  8624  wemapwe  8632  rankxplim3  8782  fseqenlem2  8886  dfac5lem4  8987  dfac2  8991  cfsuc  9117  cfflb  9119  cofsmo  9129  infpssrlem4  9166  fin4en1  9169  ssfin4  9170  fin23lem26  9185  fin23lem22  9187  fin23lem27  9188  isf34lem4  9237  isf34lem5  9238  fin1a2lem12  9271  axdc3lem2  9311  axdc4lem  9315  ttukeylem6  9374  iundom2g  9400  pwcfsdom  9443  gchen2  9486  gchor  9487  fpwwe2lem7  9496  fpwwe2lem9  9498  fpwwe2lem11  9500  fpwwe2lem12  9501  fpwwe2  9503  pwfseqlem4  9522  gchina  9559  ltexprlem6  9901  prlem936  9907  mul4  10243  2addsub  10333  muladd  10500  ltleadd  10549  leord1  10593  eqord1  10594  ltord2  10595  leord2  10596  eqord2  10597  divmul3  10728  divcan7  10772  divadddiv  10778  lemul2a  10916  lemul12b  10918  ltmuldiv2  10935  ltdivmul  10936  ledivmul  10937  ltdivmul2  10938  lt2mul2div  10939  ledivmul2  10940  lemuldiv2  10942  lt2msq  10946  ltdiv23  10952  lediv23  10953  supadd  11029  supmullem1  11031  cju  11054  zextlt  11489  suprzcl  11495  zmax  11823  xrlttr  12011  xrre3  12040  qbtwnre  12068  xrsupsslem  12175  xrinfmsslem  12176  supxrunb1  12187  supxrunb2  12188  ixxdisj  12228  iooshf  12290  icodisj  12335  iccf1o  12354  modid  12735  modadd1  12747  modmul1  12763  seqf1o  12882  expsub  12948  sqlecan  13011  bcval5  13145  hashmap  13260  hashfacen  13276  seqcoll  13286  swrdswrdlem  13505  cshwidxmod  13595  2cshwcshw  13617  cshwcshid  13619  resqreu  14037  lenegsq  14104  limsupbnd2  14258  icco1  14315  rlimresb  14340  rlimsqzlem  14423  rlimsqz  14424  rlimsqz2  14425  caucvgrlem  14447  fsum0diag2  14559  o1fsum  14589  ruclem8  15010  dvdsmulcr  15058  ndvdsadd  15181  bitsshft  15244  lcmdvds  15368  hashdvds  15527  eulerthlem2  15534  phisum  15542  pcqmul  15605  pcmpt  15643  prmreclem3  15669  4sqlem11  15706  0ram  15771  ramub1  15779  invfun  16471  initoeu2lem2  16712  coaval  16765  catcisolem  16803  funcestrcsetclem8  16834  fullestrcsetc  16838  embedsetcestrclem  16844  funcsetcestrclem8  16849  fullsetcestrc  16853  prfcl  16890  prf1st  16891  prf2nd  16892  1st2ndprf  16893  curfuncf  16925  isposd  17002  lubun  17170  isacs3lem  17213  pslem  17253  psss  17261  pwsdiagmhm  17416  gsumccat  17425  grpinvid1  17517  grpinvid2  17518  grplcan  17524  grpnpncan0  17558  dfgrp3lem  17560  dfgrp3  17561  grplactcnv  17565  0nsg  17686  eqger  17691  resghm  17723  conjghm  17738  subgga  17779  gaorber  17787  gastacl  17788  orbsta  17792  symgextf1lem  17886  psgnunilem2  17961  odid  18003  odmulg  18019  gexid  18042  odcau  18065  lsmssv  18104  lsmcom2  18116  pj1ghm  18162  frgpuptf  18229  frgpup1  18234  ghmplusg  18295  cyggex2  18344  gsumval3eu  18351  gsumval3  18354  ablfac1eu  18518  pgpfac1lem5  18524  isdrngd  18820  issrngd  18909  lmhmf1o  19094  lmhmima  19095  lmhmpreima  19096  lspextmo  19104  pwssplit2  19108  pwssplit3  19109  lspdisj  19173  islbs3  19203  lbsextlem4  19209  drngnidl  19277  lidldvgen  19303  issubassa2  19393  psrbagconf1o  19422  evlslem2  19560  ply1sclf1  19707  cnsubrg  19854  znunit  19960  cygznlem3  19966  dsmmsubg  20135  dsmmlss  20136  frlmsslsp  20183  frlmup1  20185  lindfrn  20208  f1lindf  20209  mamuass  20256  dmatmul  20351  dmatsubcl  20352  dmatmulcl  20354  dmatcrng  20356  scmataddcl  20370  scmatsubcl  20371  scmatcrng  20375  mdetunilem2  20467  pm2mpf1  20652  pm2mpghm  20669  eltg2  20810  ntrss  20907  opncldf1  20936  ssnei2  20968  neindisj  20969  restopnb  21027  restntr  21034  tgcmp  21252  hauscmplem  21257  2ndc1stc  21302  2ndcdisj  21307  2ndcomap  21309  restlly  21334  lly1stc  21347  isref  21360  islocfin  21368  comppfsc  21383  txcls  21455  txdis1cn  21486  pthaus  21489  txlm  21499  qtoptop2  21550  qtopomap  21569  kqt0lem  21587  pt1hmeo  21657  ptuncnv  21658  xkocnv  21665  fbasfip  21719  fgabs  21730  fbasrn  21735  elfm2  21799  fmfnfmlem2  21806  fmfnfmlem4  21808  ptcmplem3  21905  ptcmplem4  21906  tsmsres  21994  tsmsxplem1  22003  utoptop  22085  elbl2ps  22241  elbl2  22242  blin  22273  xmeter  22285  xmetresbl  22289  stdbdxmet  22367  metrest  22376  metustexhalf  22408  dscmet  22424  nrmmetd  22426  tngngp2  22503  nmoi2  22581  icccmplem2  22673  reconnlem2  22677  metdstri  22701  metdsle  22702  metdsre  22703  metnrmlem3  22711  fsumcn  22720  icccvx  22796  bndth  22804  evth  22805  reparphti  22843  pi1blem  22885  tchcph  23082  iscfil2  23110  cfilfcls  23118  iscau4  23123  iscauf  23124  caucfil  23127  cncmet  23165  minveclem7  23252  ovoliunlem1  23316  ovolicc2lem2  23332  ovolicc2lem3  23333  ovolicc2lem4  23334  ovolicc2lem5  23335  ovolicc2  23336  voliunlem3  23366  voliun  23368  ioombl  23379  volivth  23421  ismbfd  23452  ismbf3d  23466  itg1addlem1  23504  i1fadd  23507  itg1addlem4  23511  itg2seq  23554  itg2split  23561  itg2monolem1  23562  itg2gt0  23572  ibllem  23576  itgvallem3  23597  iblposlem  23603  dvmptfsum  23783  rolle  23798  dvlip  23801  c1liplem1  23804  lhop1  23822  lhop2  23823  dvcvx  23828  dvfsumge  23830  dvfsumrlimge0  23838  dvfsumrlim  23839  dvfsum2  23842  mdegaddle  23879  mdegvscale  23880  mdegmullem  23883  ply1divex  23941  coeeulem  24025  plyco  24042  dgrlt  24067  vieta1  24112  ulmss  24196  ulmdvlem3  24201  iblulm  24206  tanord  24329  eff1olem  24339  logdivlt  24412  logccv  24454  lawcos  24591  leibpilem1  24712  xrlimcnp  24740  cxp2limlem  24747  cxp2lim  24748  cxploglim2  24750  divsqrtsumo1  24755  lgambdd  24808  ftalem2  24845  sqff1o  24953  dvdsppwf1o  24957  dvdsflf1o  24958  musum  24962  muinv  24964  fsumdvdsmul  24966  sgmmul  24971  fsumvma  24983  logfac2  24987  chpchtsum  24989  logfacrlim  24994  logexprlim  24995  dchrelbas3  25008  dchrmulcl  25019  bposlem1  25054  lgsdchr  25125  lgsquadlem1  25150  lgsquadlem2  25151  lgsquad2lem2  25155  chebbnd1lem1  25203  chpchtlim  25213  rplogsumlem2  25219  dchrmusum2  25228  dchrvmasumlem1  25229  dchrvmasum2lem  25230  dchrvmasumlem2  25232  dchrvmasumlem3  25233  dchrvmasumiflem2  25236  dchrisum0flb  25244  dchrisum0fno1  25245  rpvmasum2  25246  dchrisum0re  25247  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0lem2  25252  dchrisum0lem3  25253  rplogsum  25261  mulogsum  25266  mulog2sumlem2  25269  vmalogdivsum2  25272  2vmadivsumlem  25274  selberglem2  25280  selberg3lem1  25291  selberg4lem1  25294  selberg4  25295  pntrsumo1  25299  selberg34r  25305  pntrlog2bndlem1  25311  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  pntibndlem3  25326  pntlemp  25344  ostthlem1  25361  ostth3  25372  ercgrg  25457  ishpg  25696  axlowdimlem15  25881  axlowdimlem16  25882  axcontlem10  25898  cusgrfilem1  26407  upgriswlk  26593  crctcshwlkn0  26769  wwlksnextwrd  26860  clwlkclwwlklem2a  26964  grpoidinv  27490  grporcan  27500  grpoinvid1  27510  grpoinvid2  27511  grpolcan  27512  ablo4  27532  nvabs  27655  sspph  27838  minvecolem7  27867  htthlem  27902  hvadd4  28021  hvaddsub4  28063  shscli  28304  pjspansn  28564  fh1  28605  fh2  28606  cm2j  28607  chscllem2  28625  spansncvi  28639  5oalem2  28642  5oalem5  28645  5oalem6  28646  3oalem2  28650  hoadd4  28771  cnvunop  28905  bralnfn  28935  eighmorth  28951  hmops  29007  hmopm  29008  adjlnop  29073  adjmul  29079  adjadd  29080  nmopcoi  29082  kbass5  29107  kbass6  29108  hstle  29217  stlesi  29228  mdsl0  29297  mdexchi  29322  atom1d  29340  superpos  29341  cvexchlem  29355  atomli  29369  atcvatlem  29372  chirredlem2  29378  chirredlem3  29379  atcvat4i  29384  mdsymlem1  29390  mdsymlem3  29392  mdsymlem5  29394  mdsymlem6  29395  sumdmdlem  29405  sumdmdlem2  29406  cdj1i  29420  opeldifid  29538  isoun  29607  1stpreimas  29611  f1od2  29627  archirngz  29871  archiabllem1  29875  archiabllem2c  29877  rngurd  29916  indf1ofs  30216  esum2d  30283  cntmeas  30417  ddemeas  30427  carsgclctunlem1  30507  itgeq12dv  30516  eulerpartlemgc  30552  eulerpartlemb  30558  eulerpartlemgs2  30570  ballotlemfc0  30682  ballotlemfcc  30683  signstfvneq0  30777  reprss  30823  reprpmtf1o  30832  hgt750lemb  30862  bnj607  31112  derangenlem  31279  subfacp1lem3  31290  subfacp1lem5  31292  cvmliftmolem2  31390  cvmliftlem6  31398  cvmlift2lem5  31415  cvmlift2lem7  31417  cvmlift2lem9  31419  mppspstlem  31594  dfon2lem6  31817  frrlem3  31907  sltres  31940  noresle  31971  nosupno  31974  colinbtwnle  32350  finminlem  32437  nn0prpwlem  32442  isfne  32459  neibastop1  32479  neibastop2lem  32480  neibastop3  32482  tailfb  32497  onsuct0  32565  nndivsub  32581  knoppcnlem6  32613  knoppndvlem9  32636  knoppndvlem18  32645  knoppndvlem21  32648  bj-finsumval0  33277  rdgeqoa  33348  matunitlindflem2  33536  poimirlem4  33543  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem25  33564  poimirlem28  33567  heicant  33574  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  mbfposadd  33587  itg2addnclem3  33593  bddiblnc  33610  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anc  33623  frinfm  33660  filbcmb  33665  seqpo  33673  sstotbnd2  33703  isbndx  33711  ssbnd  33717  prdsbnd  33722  ismtycnv  33731  ismtyres  33737  heiborlem3  33742  heibor  33750  ghomdiv  33821  grpokerinj  33822  isdrngo2  33887  rngohomco  33903  rngoisocnv  33910  rngoisoco  33911  crngm4  33932  crngohomfo  33935  isidlc  33944  ispridl2  33967  ispridlc  33999  prtlem16  34473  ax12eq  34545  ax12el  34546  lshpcmp  34593  omllaw3  34850  omlfh1N  34863  cvratlem  35025  cvrat3  35046  cvrat4  35047  ps-2  35082  elpaddn0  35404  paddasslem10  35433  cdleme0cp  35819  cdleme32a  36046  cdlemeg49lebilem  36144  cdleme50eq  36146  tendoeq2  36379  diaglbN  36661  diameetN  36662  diainN  36663  dvhopN  36722  djaclN  36742  djajN  36743  dihopelvalcpre  36854  dih1dimatlem  36935  dihmeetcl  36951  djhcl  37006  mapdpglem2  37279  ismrc  37581  eldioph2  37642  lzenom  37650  rexrabdioph  37675  fphpdo  37698  irrapxlem3  37705  elpell14qr2  37743  pell14qrreccl  37745  pell14qrdich  37750  pellfundglb  37766  monotoddzzfi  37824  2nn0ind  37827  jm2.21  37878  jm2.22  37879  dnnumch3  37934  dnwech  37935  fnwe2lem2  37938  hbtlem6  38016  imo72b2lem1  38788  cncmpmax  39505  disjf1  39683  eliccelioc  40065  fprodexp  40144  fprodabs2  40145  mullimc  40166  mullimcf  40173  islpcn  40189  limsuppnfdlem  40251  liminfval2  40318  xlimmnfvlem1  40376  xlimmnfvlem2  40377  xlimpnfvlem1  40380  xlimpnfvlem2  40381  cncfshift  40405  cncfperiod  40410  fprodcncf  40432  dvnprodlem1  40479  dvnprodlem2  40480  stoweidlem34  40569  stoweidlem48  40583  stoweidlem60  40595  fourierdlem42  40684  fourierdlem60  40701  fourierdlem61  40702  fourierdlem63  40704  fourierdlem65  40706  fourierdlem87  40728  fourierdlem97  40738  elaa2  40769  etransclem46  40815  etransc  40818  sge0iunmptlemfi  40948  isomennd  41066  ovnsslelem  41095  ovolval4lem2  41185  ovolval5lem3  41189  smflimlem3  41302  smflimlem4  41303  smflimlem6  41305  smfpimbor1lem1  41326  smflimmpt  41337  smflimsupmpt  41356  smfliminfmpt  41359  icceuelpart  41697  fmtnoprmfac2  41804  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  srhmsubc  42401  srhmsubcALTV  42419  aacllem  42875
  Copyright terms: Public domain W3C validator