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

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

Proof of Theorem simp2lr
StepHypRef Expression
1 simplr 769 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant2 1135 1 ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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  df-3an 1089
This theorem is referenced by:  fpr3g  8310  tfrlem5  8420  omeu  8623  expmordi  14207  4sqlem18  17000  vdwlem10  17028  mvrf1  22006  mdetuni0  22627  mdetmul  22629  tsmsxp  24163  ax5seglem3  28946  btwnconn1lem1  36088  btwnconn1lem3  36090  btwnconn1lem4  36091  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem7  36094  linethru  36154  lshpkrlem6  39116  athgt  39458  2llnjN  39569  dalaw  39888  cdlemb2  40043  4atexlemex6  40076  cdleme01N  40223  cdleme0ex2N  40226  cdleme7aa  40244  cdleme7e  40249  cdlemg33c0  40704  dihmeetlem3N  41307  pellex  42846
  Copyright terms: Public domain W3C validator