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

Theorem adantrr 755
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 474 . 2 ((𝜓𝜃) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 492 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  800  ad2ant2lr  801  cases2ALT  1035  consensus  1041  3adant3  1127  3ad2antr1  1204  reusv2lem3  5018  otsndisj  5127  otiunsndisj  5128  po2nr  5198  sotric  5211  sotrieq  5212  tz7.7  5908  fmptsnd  6597  fvtp1g  6625  f1cofveqaeqALT  6677  fsnex  6699  isocnv  6741  isores2  6744  isomin  6748  isoini  6749  f1oiso2  6763  ovmpt2df  6955  offval  7067  ordsucun  7188  xp1st  7363  1stconst  7431  cnvf1olem  7441  fnse  7460  mpt2xopoveq  7512  wfrlem3  7583  oalim  7779  omlim  7780  oaass  7808  omordi  7813  omwordri  7819  odi  7826  oen0  7833  oewordri  7839  nnawordi  7868  nnmordi  7878  omabs  7894  erinxp  7986  dom2lem  8159  mapen  8287  ssenen  8297  ssfi  8343  domfi  8344  domunfican  8396  mapfien  8476  ordtypelem6  8591  ordtypelem7  8592  card2inf  8623  inf3lem6  8701  cantnfle  8739  cantnflem1b  8754  cantnflem1  8757  wemapwe  8765  rankxplim3  8915  fseqenlem2  9036  dfac5lem4  9137  dfac2b  9141  dfac2OLD  9143  cfsuc  9269  cfflb  9271  cofsmo  9281  infpssrlem4  9318  fin4en1  9321  ssfin4  9322  fin23lem26  9337  fin23lem22  9339  fin23lem27  9340  isf34lem4  9389  isf34lem5  9390  fin1a2lem12  9423  axdc3lem2  9463  axdc4lem  9467  ttukeylem6  9526  iundom2g  9552  pwcfsdom  9595  gchen2  9638  gchor  9639  fpwwe2lem7  9648  fpwwe2lem9  9650  fpwwe2lem11  9652  fpwwe2lem12  9653  fpwwe2  9655  pwfseqlem4  9674  gchina  9711  ltexprlem6  10053  prlem936  10059  mul4  10395  2addsub  10485  muladd  10652  ltleadd  10701  leord1  10745  eqord1  10746  ltord2  10747  leord2  10748  eqord2  10749  divmul3  10880  divcan7  10924  divadddiv  10930  lemul2a  11068  lemul12b  11070  ltmuldiv2  11087  ltdivmul  11088  ledivmul  11089  ltdivmul2  11090  lt2mul2div  11091  ledivmul2  11092  lemuldiv2  11094  lt2msq  11098  ltdiv23  11104  lediv23  11105  supadd  11181  supmullem1  11183  cju  11206  zextlt  11641  suprzcl  11647  zmax  11976  xrlttr  12164  xrre3  12193  qbtwnre  12221  xrsupsslem  12328  xrinfmsslem  12329  supxrunb1  12340  supxrunb2  12341  ixxdisj  12381  iooshf  12443  icodisj  12488  iccf1o  12507  modid  12887  modadd1  12899  modmul1  12915  seqf1o  13034  expsub  13100  sqlecan  13163  bcval5  13297  hashmap  13412  hashfacen  13428  seqcoll  13438  swrdswrdlem  13657  cshwidxmod  13747  2cshwcshw  13769  cshwcshid  13771  resqreu  14190  lenegsq  14257  limsupbnd2  14411  icco1  14468  rlimresb  14493  rlimsqzlem  14576  rlimsqz  14577  rlimsqz2  14578  caucvgrlem  14600  fsum0diag2  14712  o1fsum  14742  ruclem8  15163  dvdsmulcr  15211  ndvdsadd  15334  bitsshft  15397  lcmdvds  15521  hashdvds  15680  eulerthlem2  15687  phisum  15695  pcqmul  15758  pcmpt  15796  prmreclem3  15822  4sqlem11  15859  0ram  15924  ramub1  15932  invfun  16623  initoeu2lem2  16864  coaval  16917  catcisolem  16955  funcestrcsetclem8  16986  fullestrcsetc  16990  embedsetcestrclem  16996  funcsetcestrclem8  17001  fullsetcestrc  17005  prfcl  17042  prf1st  17043  prf2nd  17044  1st2ndprf  17045  curfuncf  17077  isposd  17154  lubun  17322  isacs3lem  17365  pslem  17405  psss  17413  pwsdiagmhm  17568  gsumccat  17577  grpinvid1  17669  grpinvid2  17670  grplcan  17676  grpnpncan0  17710  dfgrp3lem  17712  dfgrp3  17713  grplactcnv  17717  0nsg  17838  eqger  17843  resghm  17875  conjghm  17890  subgga  17931  gaorber  17939  gastacl  17940  orbsta  17944  symgextf1lem  18038  psgnunilem2  18113  odid  18155  odmulg  18171  gexid  18194  odcau  18217  lsmssv  18256  lsmcom2  18268  pj1ghm  18314  frgpuptf  18381  frgpup1  18386  ghmplusg  18447  cyggex2  18496  gsumval3eu  18503  gsumval3  18506  ablfac1eu  18670  pgpfac1lem5  18676  isdrngd  18972  issrngd  19061  lmhmf1o  19246  lmhmima  19247  lmhmpreima  19248  lspextmo  19256  pwssplit2  19260  pwssplit3  19261  lspdisj  19325  islbs3  19355  lbsextlem4  19361  drngnidl  19429  lidldvgen  19455  issubassa2  19545  psrbagconf1o  19574  evlslem2  19712  ply1sclf1  19859  cnsubrg  20006  znunit  20112  cygznlem3  20118  dsmmsubg  20287  dsmmlss  20288  frlmsslsp  20335  frlmup1  20337  lindfrn  20360  f1lindf  20361  mamuass  20408  dmatmul  20503  dmatsubcl  20504  dmatmulcl  20506  dmatcrng  20508  scmataddcl  20522  scmatsubcl  20523  scmatcrng  20527  mdetunilem2  20619  pm2mpf1  20804  pm2mpghm  20821  eltg2  20962  ntrss  21059  opncldf1  21088  ssnei2  21120  neindisj  21121  restopnb  21179  restntr  21186  tgcmp  21404  hauscmplem  21409  2ndc1stc  21454  2ndcdisj  21459  2ndcomap  21461  restlly  21486  lly1stc  21499  isref  21512  islocfin  21520  comppfsc  21535  txcls  21607  txdis1cn  21638  pthaus  21641  txlm  21651  qtoptop2  21702  qtopomap  21721  kqt0lem  21739  pt1hmeo  21809  ptuncnv  21810  xkocnv  21817  fbasfip  21871  fgabs  21882  fbasrn  21887  elfm2  21951  fmfnfmlem2  21958  fmfnfmlem4  21960  ptcmplem3  22057  ptcmplem4  22058  tsmsres  22146  tsmsxplem1  22155  utoptop  22237  elbl2ps  22393  elbl2  22394  blin  22425  xmeter  22437  xmetresbl  22441  stdbdxmet  22519  metrest  22528  metustexhalf  22560  dscmet  22576  nrmmetd  22578  tngngp2  22655  nmoi2  22733  icccmplem2  22825  reconnlem2  22829  metdstri  22853  metdsle  22854  metdsre  22855  metnrmlem3  22863  fsumcn  22872  icccvx  22948  bndth  22956  evth  22957  reparphti  22995  pi1blem  23037  tchcph  23234  iscfil2  23262  cfilfcls  23270  iscau4  23275  iscauf  23276  caucfil  23279  cncmet  23317  minveclem7  23404  ovoliunlem1  23468  ovolicc2lem2  23484  ovolicc2lem3  23485  ovolicc2lem4  23486  ovolicc2lem5  23487  ovolicc2  23488  voliunlem3  23518  voliun  23520  ioombl  23531  volivth  23573  ismbfd  23604  ismbf3d  23618  itg1addlem1  23656  i1fadd  23659  itg1addlem4  23663  itg2seq  23706  itg2split  23713  itg2monolem1  23714  itg2gt0  23724  ibllem  23728  itgvallem3  23749  iblposlem  23755  dvmptfsum  23935  rolle  23950  dvlip  23953  c1liplem1  23956  lhop1  23974  lhop2  23975  dvcvx  23980  dvfsumge  23982  dvfsumrlimge0  23990  dvfsumrlim  23991  dvfsum2  23994  mdegaddle  24031  mdegvscale  24032  mdegmullem  24035  ply1divex  24093  coeeulem  24177  plyco  24194  dgrlt  24219  vieta1  24264  ulmss  24348  ulmdvlem3  24353  iblulm  24358  tanord  24481  eff1olem  24491  logdivlt  24564  logccv  24606  lawcos  24743  leibpilem1  24864  xrlimcnp  24892  cxp2limlem  24899  cxp2lim  24900  cxploglim2  24902  divsqrtsumo1  24907  lgambdd  24960  ftalem2  24997  sqff1o  25105  dvdsppwf1o  25109  dvdsflf1o  25110  musum  25114  muinv  25116  fsumdvdsmul  25118  sgmmul  25123  fsumvma  25135  logfac2  25139  chpchtsum  25141  logfacrlim  25146  logexprlim  25147  dchrelbas3  25160  dchrmulcl  25171  bposlem1  25206  lgsdchr  25277  lgsquadlem1  25302  lgsquadlem2  25303  lgsquad2lem2  25307  chebbnd1lem1  25355  chpchtlim  25365  rplogsumlem2  25371  dchrmusum2  25380  dchrvmasumlem1  25381  dchrvmasum2lem  25382  dchrvmasumlem2  25384  dchrvmasumlem3  25385  dchrvmasumiflem2  25388  dchrisum0flb  25396  dchrisum0fno1  25397  rpvmasum2  25398  dchrisum0re  25399  dchrisum0lem1  25402  dchrisum0lem2a  25403  dchrisum0lem2  25404  dchrisum0lem3  25405  rplogsum  25413  mulogsum  25418  mulog2sumlem2  25421  vmalogdivsum2  25424  2vmadivsumlem  25426  selberglem2  25432  selberg3lem1  25443  selberg4lem1  25446  selberg4  25447  pntrsumo1  25451  selberg34r  25457  pntrlog2bndlem1  25463  pntrlog2bndlem2  25464  pntrlog2bndlem3  25465  pntrlog2bndlem4  25466  pntrlog2bndlem5  25467  pntrlog2bndlem6  25469  pntibndlem3  25478  pntlemp  25496  ostthlem1  25513  ostth3  25524  ercgrg  25609  ishpg  25848  axlowdimlem15  26033  axlowdimlem16  26034  axcontlem10  26050  cusgrfilem1  26559  upgriswlk  26745  crctcshwlkn0  26922  wwlksnextwrd  27013  clwlkclwwlklem2a  27119  grpoidinv  27669  grporcan  27679  grpoinvid1  27689  grpoinvid2  27690  grpolcan  27691  ablo4  27711  nvabs  27834  sspph  28017  minvecolem7  28046  htthlem  28081  hvadd4  28200  hvaddsub4  28242  shscli  28483  pjspansn  28743  fh1  28784  fh2  28785  cm2j  28786  chscllem2  28804  spansncvi  28818  5oalem2  28821  5oalem5  28824  5oalem6  28825  3oalem2  28829  hoadd4  28950  cnvunop  29084  bralnfn  29114  eighmorth  29130  hmops  29186  hmopm  29187  adjlnop  29252  adjmul  29258  adjadd  29259  nmopcoi  29261  kbass5  29286  kbass6  29287  hstle  29396  stlesi  29407  mdsl0  29476  mdexchi  29501  atom1d  29519  superpos  29520  cvexchlem  29534  atomli  29548  atcvatlem  29551  chirredlem2  29557  chirredlem3  29558  atcvat4i  29563  mdsymlem1  29569  mdsymlem3  29571  mdsymlem5  29573  mdsymlem6  29574  sumdmdlem  29584  sumdmdlem2  29585  cdj1i  29599  opeldifid  29717  isoun  29786  1stpreimas  29790  f1od2  29806  archirngz  30050  archiabllem1  30054  archiabllem2c  30056  rngurd  30095  indf1ofs  30395  esum2d  30462  cntmeas  30596  ddemeas  30606  carsgclctunlem1  30686  itgeq12dv  30695  eulerpartlemgc  30731  eulerpartlemb  30737  eulerpartlemgs2  30749  ballotlemfc0  30861  ballotlemfcc  30862  signstfvneq0  30956  reprss  31002  reprpmtf1o  31011  hgt750lemb  31041  bnj607  31291  derangenlem  31458  subfacp1lem3  31469  subfacp1lem5  31471  cvmliftmolem2  31569  cvmliftlem6  31577  cvmlift2lem5  31594  cvmlift2lem7  31596  cvmlift2lem9  31598  mppspstlem  31773  dfon2lem6  31996  frrlem3  32086  sltres  32119  noresle  32150  nosupno  32153  colinbtwnle  32529  finminlem  32616  nn0prpwlem  32621  isfne  32638  neibastop1  32658  neibastop2lem  32659  neibastop3  32661  tailfb  32676  onsuct0  32744  nndivsub  32760  knoppcnlem6  32792  knoppndvlem9  32815  knoppndvlem18  32824  knoppndvlem21  32827  bj-finsumval0  33456  rdgeqoa  33527  matunitlindflem2  33717  poimirlem4  33724  poimirlem11  33731  poimirlem12  33732  poimirlem13  33733  poimirlem25  33745  poimirlem28  33748  heicant  33755  mblfinlem2  33758  mblfinlem3  33759  mblfinlem4  33760  mbfposadd  33768  itg2addnclem3  33774  bddiblnc  33791  ftc1anclem5  33800  ftc1anclem6  33801  ftc1anclem7  33802  ftc1anc  33804  frinfm  33841  filbcmb  33846  seqpo  33854  sstotbnd2  33884  isbndx  33892  ssbnd  33898  prdsbnd  33903  ismtycnv  33912  ismtyres  33918  heiborlem3  33923  heibor  33931  ghomdiv  34002  grpokerinj  34003  isdrngo2  34068  rngohomco  34084  rngoisocnv  34091  rngoisoco  34092  crngm4  34113  crngohomfo  34116  isidlc  34125  ispridl2  34148  ispridlc  34180  prtlem16  34656  ax12eq  34728  ax12el  34729  lshpcmp  34776  omllaw3  35033  omlfh1N  35046  cvratlem  35208  cvrat3  35229  cvrat4  35230  ps-2  35265  elpaddn0  35587  paddasslem10  35616  cdleme0cp  36002  cdleme32a  36229  cdlemeg49lebilem  36327  cdleme50eq  36329  tendoeq2  36562  diaglbN  36844  diameetN  36845  diainN  36846  dvhopN  36905  djaclN  36925  djajN  36926  dihopelvalcpre  37037  dih1dimatlem  37118  dihmeetcl  37134  djhcl  37189  mapdpglem2  37462  ismrc  37764  eldioph2  37825  lzenom  37833  rexrabdioph  37858  fphpdo  37881  irrapxlem3  37888  elpell14qr2  37926  pell14qrreccl  37928  pell14qrdich  37933  pellfundglb  37949  monotoddzzfi  38007  2nn0ind  38010  jm2.21  38061  jm2.22  38062  dnnumch3  38117  dnwech  38118  fnwe2lem2  38121  hbtlem6  38199  imo72b2lem1  38971  cncmpmax  39688  disjf1  39866  eliccelioc  40248  fprodexp  40327  fprodabs2  40328  mullimc  40349  mullimcf  40356  islpcn  40372  limsuppnfdlem  40434  liminfval2  40501  xlimmnfvlem1  40559  xlimmnfvlem2  40560  xlimpnfvlem1  40563  xlimpnfvlem2  40564  cncfshift  40588  cncfperiod  40593  fprodcncf  40615  dvnprodlem1  40662  dvnprodlem2  40663  stoweidlem34  40752  stoweidlem48  40766  stoweidlem60  40778  fourierdlem42  40867  fourierdlem60  40884  fourierdlem61  40885  fourierdlem63  40887  fourierdlem65  40889  fourierdlem87  40911  fourierdlem97  40921  elaa2  40952  etransclem46  40998  etransc  41001  sge0iunmptlemfi  41131  isomennd  41249  ovnsslelem  41278  ovolval4lem2  41368  ovolval5lem3  41372  smflimlem3  41485  smflimlem4  41486  smflimlem6  41488  smfpimbor1lem1  41509  smflimmpt  41520  smflimsupmpt  41539  smfliminfmpt  41542  icceuelpart  41880  fmtnoprmfac2  41987  bgoldbtbndlem2  42202  bgoldbtbndlem3  42203  srhmsubc  42584  srhmsubcALTV  42602  aacllem  43058
  Copyright terms: Public domain W3C validator