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

Theorem simp2lr 1236
 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 1129 1 ((𝜃 ∧ ((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1082 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 209  df-an 399  df-3an 1084 This theorem is referenced by:  tfrlem5  8008  omeu  8203  expmordi  13523  4sqlem18  16290  vdwlem10  16318  mvrf1  20197  mdetuni0  21222  mdetmul  21224  tsmsxp  22755  ax5seglem3  26709  fpr3g  33115  btwnconn1lem1  33541  btwnconn1lem3  33543  btwnconn1lem4  33544  btwnconn1lem5  33545  btwnconn1lem6  33546  btwnconn1lem7  33547  linethru  33607  lshpkrlem6  36243  athgt  36584  2llnjN  36695  dalaw  37014  cdlemb2  37169  4atexlemex6  37202  cdleme01N  37349  cdleme0ex2N  37352  cdleme7aa  37370  cdleme7e  37375  cdlemg33c0  37830  dihmeetlem3N  38433  pellex  39422
 Copyright terms: Public domain W3C validator