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

Theorem adantllr 751
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 472 . 2 ((𝜑𝜏) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 680 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 196  df-an 385
This theorem is referenced by:  adantl3r  782  r19.29an  3059  elsnxpOLD  5595  oewordri  7559  marypha1lem  8222  gruwun  9514  lemul12b  10759  rlimsqzlem  14227  fsumrlim  14384  fsumo1  14385  lcmdvds  15159  isacs2  16137  dfgrp3lem  17336  tgcl  20584  neindisj  20731  neiptoptop  20745  isr0  21350  cnextcn  21681  ustuqtop4  21858  metss  22123  mbfsup  23237  itg2i1fseqle  23327  ditgsplit  23431  itgulm  23966  leibpi  24469  dchrisumlem3  24980  iscgrglt  25209  legov  25280  legov2  25281  legtrid  25286  colopp  25461  f1otrg  25551  cusgrasize2inds  26005  grpoidinvlem3  26744  grpoideu  26747  grporcan  26756  blocni  27044  normcan  27819  unoplin  28163  hmoplin  28185  nmophmi  28274  mdslmd3i  28575  chirredlem1  28633  chirredlem2  28634  mdsymlem5  28650  cdj1i  28676  fpwrelmap  28896  archiabllem1  29078  archiabl  29083  isarchiofld  29148  locfinreflem  29235  pstmxmet  29268  ordtconlem1  29298  esumcvg  29475  esum2d  29482  esumiun  29483  ldgenpisyslem1  29553  omssubadd  29689  signstfvneq0  29975  elicc3  31481  knoppcnlem9  31661  lindsenlbs  32574  matunitlindflem1  32575  poimirlem17  32596  poimirlem20  32599  poimirlem27  32606  poimirlem29  32608  poimir  32612  heicant  32614  itg2addnclem  32631  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  fzmul  32707  fdc  32711  fdc1  32712  incsequz2  32715  rrncmslem  32801  ghomco  32860  rngoisocnv  32950  ispridlc  33039  cvgdvgrat  37534  binomcxplemnotnn0  37577  founiiun0  38372  supxrge  38495  suplesup  38496  lptre2pt  38707  0ellimcdiv  38716  limclner  38718  icccncfext  38773  cncfiooiccre  38781  fperdvper  38808  dvnprodlem2  38837  iblcncfioo  38870  stoweidlem35  38928  wallispilem3  38960  fourierdlem20  39020  fourierdlem34  39034  fourierdlem39  39039  fourierdlem42  39042  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem63  39062  fourierdlem64  39063  fourierdlem73  39072  fourierdlem87  39086  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  etransclem32  39159  etransclem33  39160  etransclem35  39162  sge0cl  39274  sge0f1o  39275  sge0split  39302  sge0iunmptlemre  39308  sge0rpcpnf  39314  sge0xadd  39328  nnfoctbdjlem  39348  ismeannd  39360  omeiunltfirp  39409  hoidmvlelem3  39487  hoidmvle  39490  ovncvr2  39501  hspdifhsp  39506  hspmbllem2  39517  ovnsubadd2lem  39535  pimdecfgtioo  39604  pimincfltioo  39605  smflimlem1  39657  cusgrsize2inds  40669  aacllem  42356
  Copyright terms: Public domain W3C validator