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

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

Proof of Theorem simp2lr
StepHypRef Expression
1 simplr 791 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant2 1081 1 ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036 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 386  df-3an 1038 This theorem is referenced by:  tfrlem5  7421  omeu  7610  4sqlem18  15590  vdwlem10  15618  mvrf1  19344  mdetuni0  20346  mdetmul  20348  tsmsxp  21868  ax5seglem3  25711  btwnconn1lem1  31836  btwnconn1lem3  31838  btwnconn1lem4  31839  btwnconn1lem5  31840  btwnconn1lem6  31841  btwnconn1lem7  31842  linethru  31902  lshpkrlem6  33882  athgt  34222  2llnjN  34333  dalaw  34652  cdlemb2  34807  4atexlemex6  34840  cdleme01N  34988  cdleme0ex2N  34991  cdleme7aa  35009  cdleme7e  35014  cdlemg33c0  35470  dihmeetlem3N  36074  pellex  36879  expmordi  36992
 Copyright terms: Public domain W3C validator