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

Theorem adantlrl 756
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 476 . 2 ((𝜏𝜓) → 𝜓)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl2 684 1 (((𝜑 ∧ (𝜏𝜓)) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  omlimcl  7703  odi  7704  oelim2  7720  mapxpen  8167  unwdomg  8530  dfac12lem2  9004  infunsdom  9074  fin1a2s  9274  frlmup1  20185  fbasrn  21735  lmmbr  23102  grporcan  27500  unoplin  28907  hmoplin  28929  superpos  29341  subfacp1lem5  31292  matunitlindflem1  33535  poimirlem4  33543  itg2addnclem  33591  ftc1anclem6  33620  fdc  33671  ismtyres  33737  isdrngo2  33887  rngohomco  33903  rngoisocnv  33910  dssmapnvod  38631  climxrrelem  40299  dvdsn1add  40472  dvnprodlem1  40479  stoweidlem27  40562  fourierdlem97  40738  qndenserrnbllem  40832  sge0iunmptlemfi  40948
  Copyright terms: Public domain W3C validator