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

Theorem adantlrr 717
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 483 . 2 ((𝜓𝜏) → 𝜓)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl2 677 1 (((𝜑 ∧ (𝜓𝜏)) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  disjxiun  5054  2ndconst  7785  oelim  8148  odi  8194  marypha1lem  8885  dfac12lem2  9558  infunsdom  9624  isf34lem4  9787  distrlem1pr  10435  lcmgcdlem  15938  lcmdvds  15940  drsdirfi  17536  isacs3lem  17764  conjnmzb  18331  psgndif  20674  frlmsslsp  20868  metss2lem  23048  nghmcn  23281  bndth  23489  itg2monolem1  24278  dvmptfsum  24499  ply1divex  24657  itgulm  24923  rpvmasumlem  25990  dchrmusum2  25997  dchrisum0lem2  26021  dchrisum0lem3  26022  mulog2sumlem2  26038  pntibndlem3  26095  wwlksubclwwlk  27764  blocni  28509  superpos  30058  chirredlem2  30095  eulerpartlemgvv  31533  ballotlemfc0  31649  ballotlemfcc  31650  bj-finsumval0  34455  pibt2  34580  fin2solem  34759  matunitlindflem1  34769  poimirlem28  34801  heicant  34808  ftc1anclem6  34853  ftc1anc  34856  fdc  34901  incsequz  34904  ismtyres  34967  isdrngo2  35117  rngohomco  35133  keridl  35191  linepsubN  36768  pmapsub  36784  mzpcompact2lem  39226  pellex  39310  monotuz  39416  unxpwdom3  39573  dssmapnvod  40244  radcnvrat  40523  fprodexp  41751  fprodabs2  41752  climxrrelem  41906  dvnprodlem1  42107  stoweidlem34  42196  fourierdlem42  42311  elaa2  42396  sge0iunmptlemfi  42572  aacllem  44830
  Copyright terms: Public domain W3C validator