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

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

Proof of Theorem adantlrl
StepHypRef Expression
1 simpr 488 . 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:  1stconst  7782  omlimcl  8191  odi  8192  oelim2  8208  mapxpen  8671  unwdomg  9036  dfac12lem2  9559  infunsdom  9629  fin1a2s  9829  ccatpfx  14058  frlmup1  20490  fbasrn  22492  lmmbr  23865  grporcan  28304  unoplin  29706  hmoplin  29728  superpos  30140  ccatf1  30654  subfacp1lem5  32539  matunitlindflem1  35046  poimirlem4  35054  itg2addnclem  35101  ftc1anclem6  35128  fdc  35176  ismtyres  35239  isdrngo2  35389  rngohomco  35405  rngoisocnv  35412  dssmapnvod  40708  climxrrelem  42378  dvdsn1add  42568  dvnprodlem1  42575  stoweidlem27  42656  fourierdlem97  42832  qndenserrnbllem  42923  sge0iunmptlemfi  43039
  Copyright terms: Public domain W3C validator