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

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

Proof of Theorem simp2lr
StepHypRef Expression
1 simplr 767 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant2 1134 1 ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  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 206  df-an 397  df-3an 1089
This theorem is referenced by:  fpr3g  8272  tfrlem5  8382  omeu  8587  expmordi  14136  4sqlem18  16899  vdwlem10  16927  mvrf1  21764  mdetuni0  22343  mdetmul  22345  tsmsxp  23879  ax5seglem3  28444  btwnconn1lem1  35351  btwnconn1lem3  35353  btwnconn1lem4  35354  btwnconn1lem5  35355  btwnconn1lem6  35356  btwnconn1lem7  35357  linethru  35417  lshpkrlem6  38288  athgt  38630  2llnjN  38741  dalaw  39060  cdlemb2  39215  4atexlemex6  39248  cdleme01N  39395  cdleme0ex2N  39398  cdleme7aa  39416  cdleme7e  39421  cdlemg33c0  39876  dihmeetlem3N  40479  pellex  41875
  Copyright terms: Public domain W3C validator