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

Theorem adantllr 718
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
Hypothesis
Ref Expression
adantl2.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
adantllr ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem adantllr
StepHypRef Expression
1 simpl 484 . 2 ((𝜑𝜏) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 679 1 ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  ad4ant13  750  ad4ant134  1175  ad5ant145  1370  oewordri  8540  marypha1lem  9370  rlimsqzlem  15534  fsumrlim  15697  fsumo1  15698  lcmdvds  16485  dfgrp3lem  18846  tgcl  22322  neindisj  22471  neiptoptop  22485  isr0  23091  cnextcn  23421  ustuqtop4  23599  mbfsup  25031  itg2i1fseqle  25122  ditgsplit  25228  itgulm  25770  leibpi  26295  dchrisumlem3  26842  legov  27530  legov2  27531  legtrid  27536  colopp  27714  f1otrg  27816  cusgrsize2inds  28404  grpoidinvlem3  29451  grpoideu  29454  grporcan  29463  blocni  29750  normcan  30521  unoplin  30865  hmoplin  30887  nmophmi  30976  mdslmd3i  31277  chirredlem1  31335  chirredlem2  31336  mdsymlem5  31352  cdj1i  31378  opreu2reuALT  31408  fpwrelmap  31653  fsumiunle  31728  ccatf1  31808  wrdt2ind  31810  archiabllem1  32032  archiabl  32037  isarchiofld  32115  ringlsmss1  32180  ringlsmss2  32181  nsgqusf1olem1  32194  nsgqusf1olem2  32195  nsgqusf1olem3  32196  rhmimaidl  32209  isprmidlc  32223  fedgmul  32329  irngnzply1  32368  locfinreflem  32424  pstmxmet  32481  ordtconnlem1  32508  esumcvg  32688  esum2d  32695  esumiun  32696  ldgenpisyslem1  32765  omssubadd  32903  signstfvneq0  33187  circlemeth  33256  elicc3  34792  knoppcnlem9  34967  pibt2  35891  lindsenlbs  36076  matunitlindflem1  36077  poimirlem17  36098  poimirlem20  36101  poimirlem27  36108  poimirlem29  36110  poimir  36114  heicant  36116  itg2addnclem  36132  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  fzmul  36203  fdc  36207  fdc1  36208  incsequz2  36211  rrncmslem  36294  ghomco  36353  rngoisocnv  36443  ispridlc  36532  fsuppind  40768  cvgdvgrat  42600  binomcxplemnotnn0  42643  founiiun0  43416  supxrge  43579  suplesup  43580  supxrunb3  43641  lptre2pt  43888  0ellimcdiv  43897  limclner  43899  limsuppnfdlem  43949  limsuppnflem  43958  limsupmnflem  43968  liminfreuzlem  44050  liminflimsupclim  44055  cnrefiisplem  44077  climxlim2lem  44093  xlimliminflimsup  44110  icccncfext  44135  cncfiooiccre  44143  fperdvper  44167  dvnprodlem2  44195  iblcncfioo  44226  stoweidlem35  44283  wallispilem3  44315  fourierdlem20  44375  fourierdlem34  44389  fourierdlem39  44394  fourierdlem42  44397  fourierdlem46  44400  fourierdlem48  44402  fourierdlem49  44403  fourierdlem63  44417  fourierdlem64  44418  fourierdlem73  44427  fourierdlem87  44441  fourierdlem97  44451  fourierdlem103  44457  fourierdlem104  44458  fourierdlem111  44465  etransclem32  44514  etransclem33  44515  etransclem35  44517  sge0cl  44629  sge0f1o  44630  sge0split  44657  sge0iunmptlemre  44663  sge0rpcpnf  44669  sge0xadd  44683  nnfoctbdjlem  44703  ismeannd  44715  omeiunltfirp  44767  hoidmvlelem3  44845  hoidmvle  44848  ovncvr2  44859  hspdifhsp  44864  hspmbllem2  44875  ovnsubadd2lem  44893  pimdecfgtioo  44965  pimincfltioo  44966  smflimlem1  45019  smflimmpt  45058  smfpimne2  45088  aacllem  47255
  Copyright terms: Public domain W3C validator