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

Theorem simp3rr 1239
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 1127 1 ((𝜃𝜏 ∧ (𝜒 ∧ (𝜑𝜓))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 1081
This theorem is referenced by:  omeu  8200  ntrivcvgmul  15246  tsmsxp  22690  tgqioo  23335  ovolunlem2  24026  plyadd  24734  plymul  24735  coeeu  24742  tghilberti2  26351  cvmlift2lem10  32456  nosupbnd1lem2  33106  btwnconn1lem1  33445  lplnexllnN  36580  2llnjN  36583  4atlem12b  36627  lplncvrlvol2  36631  lncmp  36799  cdlema2N  36808  cdleme11a  37276  cdleme24  37368  cdleme28  37389  cdlemefr29bpre0N  37422  cdlemefr29clN  37423  cdlemefr32fvaN  37425  cdlemefr32fva1  37426  cdlemefs29bpre0N  37432  cdlemefs29bpre1N  37433  cdlemefs29cpre1N  37434  cdlemefs29clN  37435  cdlemefs32fvaN  37438  cdlemefs32fva1  37439  cdleme36m  37477  cdleme17d3  37512  cdlemg36  37730  cdlemj3  37839  cdlemkid1  37938  cdlemk19ylem  37946  cdlemk19xlem  37958  dihlsscpre  38250  dihord4  38274  dihmeetlem1N  38306  dihatlat  38350  jm2.27  39483
  Copyright terms: Public domain W3C validator