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

Theorem simp2lr 1306
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp2lr ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)

Proof of Theorem simp2lr
StepHypRef Expression
1 simplr 744 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant2 1127 1 ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1070
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  df-3an 1072
This theorem is referenced by:  tfrlem5  7628  omeu  7818  4sqlem18  15872  vdwlem10  15900  mvrf1  19639  mdetuni0  20644  mdetmul  20646  tsmsxp  22177  ax5seglem3  26031  btwnconn1lem1  32525  btwnconn1lem3  32527  btwnconn1lem4  32528  btwnconn1lem5  32529  btwnconn1lem6  32530  btwnconn1lem7  32531  linethru  32591  lshpkrlem6  34917  athgt  35257  2llnjN  35368  dalaw  35687  cdlemb2  35842  4atexlemex6  35875  cdleme01N  36023  cdleme0ex2N  36026  cdleme7aa  36044  cdleme7e  36049  cdlemg33c0  36504  dihmeetlem3N  37108  pellex  37918  expmordi  38031
  Copyright terms: Public domain W3C validator