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

Theorem adantlrl 699
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 471 . 2 ((𝜏𝜓) → 𝜓)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl2 660 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 197  df-an 383
This theorem is referenced by:  omlimcl  7812  odi  7813  oelim2  7829  mapxpen  8282  unwdomg  8645  dfac12lem2  9168  infunsdom  9238  fin1a2s  9438  frlmup1  20354  fbasrn  21908  lmmbr  23275  grporcan  27712  unoplin  29119  hmoplin  29141  superpos  29553  subfacp1lem5  31504  matunitlindflem1  33738  poimirlem4  33746  itg2addnclem  33793  ftc1anclem6  33822  fdc  33873  ismtyres  33939  isdrngo2  34089  rngohomco  34105  rngoisocnv  34112  dssmapnvod  38840  climxrrelem  40499  dvdsn1add  40672  dvnprodlem1  40679  stoweidlem27  40761  fourierdlem97  40937  qndenserrnbllem  41031  sge0iunmptlemfi  41147
  Copyright terms: Public domain W3C validator