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

Theorem adantlrl 718
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 485 . 2 ((𝜏𝜓) → 𝜓)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl2 679 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 206  df-an 397
This theorem is referenced by:  1stconst  8024  omlimcl  8517  odi  8518  oelim2  8534  mapxpen  9045  unwdomg  9478  dfac12lem2  10038  infunsdom  10108  fin1a2s  10308  ccatpfx  14543  frlmup1  21151  fbasrn  23181  lmmbr  24568  grporcan  29305  unoplin  30707  hmoplin  30729  superpos  31141  ccatf1  31647  subfacp1lem5  33606  matunitlindflem1  36006  poimirlem4  36014  itg2addnclem  36061  ftc1anclem6  36088  fdc  36136  ismtyres  36199  isdrngo2  36349  rngohomco  36365  rngoisocnv  36372  dssmapnvod  42197  climxrrelem  43885  dvdsn1add  44075  dvnprodlem1  44082  stoweidlem27  44163  fourierdlem97  44339  qndenserrnbllem  44430  sge0iunmptlemfi  44549
  Copyright terms: Public domain W3C validator