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

Theorem adantlrr 719
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 481 . 2 ((𝜓𝜏) → 𝜓)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl2 679 1 (((𝜑 ∧ (𝜓𝜏)) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  disjxiun  5146  2ndconst  8106  oelim  8555  odi  8600  marypha1lem  9458  dfac12lem2  10169  infunsdom  10239  isf34lem4  10402  distrlem1pr  11050  lcmgcdlem  16580  lcmdvds  16582  drsdirfi  18300  isacs3lem  18537  conjnmzb  19216  psgndif  21551  frlmsslsp  21747  metss2lem  24464  nghmcn  24706  bndth  24928  itg2monolem1  25724  dvmptfsum  25951  ply1divex  26117  itgulm  26389  rpvmasumlem  27465  dchrmusum2  27472  dchrisum0lem2  27496  dchrisum0lem3  27497  mulog2sumlem2  27513  pntibndlem3  27570  wwlksubclwwlk  29940  blocni  30687  superpos  32236  chirredlem2  32273  eulerpartlemgvv  34127  ballotlemfc0  34243  ballotlemfcc  34244  bj-finsumval0  36895  pibt2  37027  fin2solem  37210  matunitlindflem1  37220  poimirlem28  37252  heicant  37259  ftc1anclem6  37302  ftc1anc  37305  fdc  37349  incsequz  37352  ismtyres  37412  isdrngo2  37562  rngohomco  37578  keridl  37636  linepsubN  39355  pmapsub  39371  fsuppind  41958  mhpind  41962  mzpcompact2lem  42313  pellex  42397  monotuz  42504  unxpwdom3  42661  cantnfresb  42895  dssmapnvod  43592  radcnvrat  43893  fprodexp  45120  fprodabs2  45121  climxrrelem  45275  dvnprodlem1  45472  stoweidlem34  45560  fourierdlem42  45675  elaa2  45760  sge0iunmptlemfi  45939  aacllem  48420
  Copyright terms: Public domain W3C validator