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

Theorem simp2lr 1240
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 1133 1 ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 1088
This theorem is referenced by:  fpr3g  8309  tfrlem5  8419  omeu  8622  expmordi  14204  4sqlem18  16996  vdwlem10  17024  mvrf1  22024  mdetuni0  22643  mdetmul  22645  tsmsxp  24179  ax5seglem3  28961  btwnconn1lem1  36069  btwnconn1lem3  36071  btwnconn1lem4  36072  btwnconn1lem5  36073  btwnconn1lem6  36074  btwnconn1lem7  36075  linethru  36135  lshpkrlem6  39097  athgt  39439  2llnjN  39550  dalaw  39869  cdlemb2  40024  4atexlemex6  40057  cdleme01N  40204  cdleme0ex2N  40207  cdleme7aa  40225  cdleme7e  40230  cdlemg33c0  40685  dihmeetlem3N  41288  pellex  42823
  Copyright terms: Public domain W3C validator