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 486 . 2 ((𝜓𝜏) → 𝜓)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl2 680 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:  disjxiun  5030  2ndconst  7783  oelim  8146  odi  8192  marypha1lem  8885  dfac12lem2  9559  infunsdom  9629  isf34lem4  9792  distrlem1pr  10440  lcmgcdlem  15944  lcmdvds  15946  drsdirfi  17544  isacs3lem  17772  conjnmzb  18389  psgndif  20295  frlmsslsp  20489  metss2lem  23122  nghmcn  23355  bndth  23567  itg2monolem1  24358  dvmptfsum  24582  ply1divex  24741  itgulm  25007  rpvmasumlem  26075  dchrmusum2  26082  dchrisum0lem2  26106  dchrisum0lem3  26107  mulog2sumlem2  26123  pntibndlem3  26180  wwlksubclwwlk  27847  blocni  28592  superpos  30141  chirredlem2  30178  eulerpartlemgvv  31748  ballotlemfc0  31864  ballotlemfcc  31865  bj-finsumval0  34701  pibt2  34835  fin2solem  35042  matunitlindflem1  35052  poimirlem28  35084  heicant  35091  ftc1anclem6  35134  ftc1anc  35137  fdc  35182  incsequz  35185  ismtyres  35245  isdrngo2  35395  rngohomco  35411  keridl  35469  linepsubN  37047  pmapsub  37063  fsuppind  39453  mzpcompact2lem  39689  pellex  39773  monotuz  39879  unxpwdom3  40036  dssmapnvod  40718  radcnvrat  41015  fprodexp  42233  fprodabs2  42234  climxrrelem  42388  dvnprodlem1  42585  stoweidlem34  42673  fourierdlem42  42788  elaa2  42873  sge0iunmptlemfi  43049  aacllem  45326
  Copyright terms: Public domain W3C validator