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

Theorem adantlrr 720
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
adantlrr (((𝜑 ∧ (𝜓𝜏)) ∧ 𝜒) → 𝜃)

Proof of Theorem adantlrr
StepHypRef Expression
1 simpl 484 . 2 ((𝜓𝜏) → 𝜓)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl2 680 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:  disjxiun  5103  2ndconst  8034  oelim  8481  odi  8527  marypha1lem  9370  dfac12lem2  10081  infunsdom  10151  isf34lem4  10314  distrlem1pr  10962  lcmgcdlem  16483  lcmdvds  16485  drsdirfi  18195  isacs3lem  18432  conjnmzb  19044  psgndif  21009  frlmsslsp  21205  metss2lem  23870  nghmcn  24112  bndth  24324  itg2monolem1  25118  dvmptfsum  25342  ply1divex  25504  itgulm  25770  rpvmasumlem  26838  dchrmusum2  26845  dchrisum0lem2  26869  dchrisum0lem3  26870  mulog2sumlem2  26886  pntibndlem3  26943  wwlksubclwwlk  29005  blocni  29750  superpos  31299  chirredlem2  31336  eulerpartlemgvv  32979  ballotlemfc0  33095  ballotlemfcc  33096  bj-finsumval0  35759  pibt2  35891  fin2solem  36067  matunitlindflem1  36077  poimirlem28  36109  heicant  36116  ftc1anclem6  36159  ftc1anc  36162  fdc  36207  incsequz  36210  ismtyres  36270  isdrngo2  36420  rngohomco  36436  keridl  36494  linepsubN  38218  pmapsub  38234  fsuppind  40768  mhpind  40772  mzpcompact2lem  41077  pellex  41161  monotuz  41268  unxpwdom3  41425  cantnfresb  41661  dssmapnvod  42299  radcnvrat  42601  fprodexp  43842  fprodabs2  43843  climxrrelem  43997  dvnprodlem1  44194  stoweidlem34  44282  fourierdlem42  44397  elaa2  44482  sge0iunmptlemfi  44661  aacllem  47255
  Copyright terms: Public domain W3C validator