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

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

Proof of Theorem simp2lr
StepHypRef Expression
1 simplr 766 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant2 1131 1 ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1084
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 396  df-3an 1086
This theorem is referenced by:  fpr3g  8271  tfrlem5  8381  omeu  8586  expmordi  14137  4sqlem18  16904  vdwlem10  16932  mvrf1  21887  mdetuni0  22478  mdetmul  22480  tsmsxp  24014  ax5seglem3  28697  btwnconn1lem1  35592  btwnconn1lem3  35594  btwnconn1lem4  35595  btwnconn1lem5  35596  btwnconn1lem6  35597  btwnconn1lem7  35598  linethru  35658  lshpkrlem6  38498  athgt  38840  2llnjN  38951  dalaw  39270  cdlemb2  39425  4atexlemex6  39458  cdleme01N  39605  cdleme0ex2N  39608  cdleme7aa  39626  cdleme7e  39631  cdlemg33c0  40086  dihmeetlem3N  40689  pellex  42156
  Copyright terms: Public domain W3C validator