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

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

Proof of Theorem simp3rr
StepHypRef Expression
1 simprr 780 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant3 1158 1 ((𝜃𝜏 ∧ (𝜒 ∧ (𝜑𝜓))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  omeu  7902  ntrivcvgmul  14855  tsmsxp  22171  tgqioo  22816  ovolunlem2  23479  plyadd  24187  plymul  24188  coeeu  24195  tghilberti2  25747  cvmlift2lem10  31617  nosupbnd1lem2  32176  btwnconn1lem1  32515  lplnexllnN  35344  2llnjN  35347  4atlem12b  35391  lplncvrlvol2  35395  lncmp  35563  cdlema2N  35572  cdleme11a  36041  cdleme24  36133  cdleme28  36154  cdlemefr29bpre0N  36187  cdlemefr29clN  36188  cdlemefr32fvaN  36190  cdlemefr32fva1  36191  cdlemefs29bpre0N  36197  cdlemefs29bpre1N  36198  cdlemefs29cpre1N  36199  cdlemefs29clN  36200  cdlemefs32fvaN  36203  cdlemefs32fva1  36204  cdleme36m  36242  cdleme17d3  36277  cdlemg36  36495  cdlemj3  36604  cdlemkid1  36703  cdlemk19ylem  36711  cdlemk19xlem  36723  dihlsscpre  37015  dihord4  37039  dihmeetlem1N  37071  dihatlat  37115  jm2.27  38076
  Copyright terms: Public domain W3C validator