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

Theorem adantlrl 751
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 475 . 2 ((𝜏𝜓) → 𝜓)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl2 680 1 (((𝜑 ∧ (𝜏𝜓)) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  omlimcl  7518  odi  7519  oelim2  7535  mapxpen  7984  unwdomg  8345  dfac12lem2  8822  infunsdom  8892  fin1a2s  9092  frlmup1  19894  fbasrn  21436  lmmbr  22778  grporcan  26518  unoplin  27965  hmoplin  27987  superpos  28399  subfacp1lem5  30222  matunitlindflem1  32374  poimirlem4  32382  itg2addnclem  32430  ftc1anclem6  32459  fdc  32510  ismtyres  32576  isdrngo2  32726  rngohomco  32742  rngoisocnv  32749  dssmapnvod  37133  dvdsn1add  38629  dvnprodlem1  38636  stoweidlem27  38720  fourierdlem97  38896  qndenserrnbllem  38990  sge0iunmptlemfi  39106
  Copyright terms: Public domain W3C validator