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 768 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant2 1135 1 ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  fpr3g  8220  tfrlem5  8330  omeu  8536  expmordi  14081  4sqlem18  16842  vdwlem10  16870  mvrf1  21417  mdetuni0  21993  mdetmul  21995  tsmsxp  23529  ax5seglem3  27929  btwnconn1lem1  34725  btwnconn1lem3  34727  btwnconn1lem4  34728  btwnconn1lem5  34729  btwnconn1lem6  34730  btwnconn1lem7  34731  linethru  34791  lshpkrlem6  37627  athgt  37969  2llnjN  38080  dalaw  38399  cdlemb2  38554  4atexlemex6  38587  cdleme01N  38734  cdleme0ex2N  38737  cdleme7aa  38755  cdleme7e  38760  cdlemg33c0  39215  dihmeetlem3N  39818  pellex  41205
  Copyright terms: Public domain W3C validator