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 486 . 2 ((𝜑𝜏) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 679 1 ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  ad4ant13  750  ad4ant134  1171  ad5ant145  1366  r19.29anOLD  3324  oewordri  8210  marypha1lem  8890  rlimsqzlem  15003  fsumrlim  15164  fsumo1  15165  lcmdvds  15948  dfgrp3lem  18195  tgcl  21572  neindisj  21720  neiptoptop  21734  isr0  22340  cnextcn  22670  ustuqtop4  22848  mbfsup  24266  itg2i1fseqle  24356  ditgsplit  24462  itgulm  25001  leibpi  25526  dchrisumlem3  26073  legov  26377  legov2  26378  legtrid  26383  colopp  26561  f1otrg  26663  cusgrsize2inds  27241  grpoidinvlem3  28287  grpoideu  28290  grporcan  28299  blocni  28586  normcan  29357  unoplin  29701  hmoplin  29723  nmophmi  29812  mdslmd3i  30113  chirredlem1  30171  chirredlem2  30172  mdsymlem5  30188  cdj1i  30214  opreu2reuALT  30244  fpwrelmap  30475  fsumiunle  30551  ccatf1  30631  wrdt2ind  30633  archiabllem1  30849  archiabl  30854  isarchiofld  30917  isprmidlc  30993  fedgmul  31057  locfinreflem  31134  pstmxmet  31167  ordtconnlem1  31194  esumcvg  31372  esum2d  31379  esumiun  31380  ldgenpisyslem1  31449  omssubadd  31585  signstfvneq0  31869  circlemeth  31938  elicc3  33692  knoppcnlem9  33867  pibt2  34748  lindsenlbs  34964  matunitlindflem1  34965  poimirlem17  34986  poimirlem20  34989  poimirlem27  34996  poimirlem29  34998  poimir  35002  heicant  35004  itg2addnclem  35020  ftc1anclem5  35046  ftc1anclem6  35047  ftc1anclem7  35048  ftc1anclem8  35049  ftc1anc  35050  fzmul  35091  fdc  35095  fdc1  35096  incsequz2  35099  rrncmslem  35182  ghomco  35241  rngoisocnv  35331  ispridlc  35420  cvgdvgrat  40877  binomcxplemnotnn0  40920  founiiun0  41682  supxrge  41836  suplesup  41837  supxrunb3  41902  lptre2pt  42148  0ellimcdiv  42157  limclner  42159  limsuppnfdlem  42209  limsuppnflem  42218  limsupmnflem  42228  liminfreuzlem  42310  liminflimsupclim  42315  cnrefiisplem  42337  climxlim2lem  42353  xlimliminflimsup  42370  icccncfext  42395  cncfiooiccre  42403  fperdvper  42427  dvnprodlem2  42455  iblcncfioo  42486  stoweidlem35  42543  wallispilem3  42575  fourierdlem20  42635  fourierdlem34  42649  fourierdlem39  42654  fourierdlem42  42657  fourierdlem46  42660  fourierdlem48  42662  fourierdlem49  42663  fourierdlem63  42677  fourierdlem64  42678  fourierdlem73  42687  fourierdlem87  42701  fourierdlem97  42711  fourierdlem103  42717  fourierdlem104  42718  fourierdlem111  42725  etransclem32  42774  etransclem33  42775  etransclem35  42777  sge0cl  42886  sge0f1o  42887  sge0split  42914  sge0iunmptlemre  42920  sge0rpcpnf  42926  sge0xadd  42940  nnfoctbdjlem  42960  ismeannd  42972  omeiunltfirp  43024  hoidmvlelem3  43102  hoidmvle  43105  ovncvr2  43116  hspdifhsp  43121  hspmbllem2  43132  ovnsubadd2lem  43150  pimdecfgtioo  43218  pimincfltioo  43219  smflimlem1  43270  smflimmpt  43307  aacllem  45183
  Copyright terms: Public domain W3C validator