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

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

Proof of Theorem adantlrl
StepHypRef Expression
1 simpr 484 . 2 ((𝜏𝜓) → 𝜓)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl2 681 1 (((𝜑 ∧ (𝜏𝜓)) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  1stconst  8125  omlimcl  8616  odi  8617  oelim2  8633  mapxpen  9183  unwdomg  9624  dfac12lem2  10185  infunsdom  10253  fin1a2s  10454  ccatpfx  14739  frlmup1  21818  fbasrn  23892  lmmbr  25292  grporcan  30537  unoplin  31939  hmoplin  31961  superpos  32373  ccatf1  32933  subfacp1lem5  35189  matunitlindflem1  37623  poimirlem4  37631  itg2addnclem  37678  ftc1anclem6  37705  fdc  37752  ismtyres  37815  isdrngo2  37965  rngohomco  37981  rngoisocnv  37988  dssmapnvod  44033  climxrrelem  45764  dvdsn1add  45954  dvnprodlem1  45961  stoweidlem27  46042  fourierdlem97  46218  qndenserrnbllem  46309  sge0iunmptlemfi  46428
  Copyright terms: Public domain W3C validator