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

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

Proof of Theorem simp3rr
StepHypRef Expression
1 simprr 769 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant3 1129 1 ((𝜃𝜏 ∧ (𝜒 ∧ (𝜑𝜓))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  omeu  8201  ntrivcvgmul  15248  tsmsxp  22678  tgqioo  23323  ovolunlem2  24014  plyadd  24722  plymul  24723  coeeu  24730  tghilberti2  26338  cvmlift2lem10  32443  nosupbnd1lem2  33093  btwnconn1lem1  33432  lplnexllnN  36567  2llnjN  36570  4atlem12b  36614  lplncvrlvol2  36618  lncmp  36786  cdlema2N  36795  cdleme11a  37263  cdleme24  37355  cdleme28  37376  cdlemefr29bpre0N  37409  cdlemefr29clN  37410  cdlemefr32fvaN  37412  cdlemefr32fva1  37413  cdlemefs29bpre0N  37419  cdlemefs29bpre1N  37420  cdlemefs29cpre1N  37421  cdlemefs29clN  37422  cdlemefs32fvaN  37425  cdlemefs32fva1  37426  cdleme36m  37464  cdleme17d3  37499  cdlemg36  37717  cdlemj3  37826  cdlemkid1  37925  cdlemk19ylem  37933  cdlemk19xlem  37945  dihlsscpre  38237  dihord4  38261  dihmeetlem1N  38293  dihatlat  38337  jm2.27  39470
  Copyright terms: Public domain W3C validator