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

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

Proof of Theorem simp3rr
StepHypRef Expression
1 simprr 771 . 2 ((𝜒 ∧ (𝜑𝜓)) → 𝜓)
213ad2ant3 1132 1 ((𝜃𝜏 ∧ (𝜒 ∧ (𝜑𝜓))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084
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 395  df-3an 1086
This theorem is referenced by:  poxp3  8161  omeu  8612  ntrivcvgmul  15888  tsmsxp  24079  tgqioo  24736  ovolunlem2  25447  plyadd  26171  plymul  26172  coeeu  26179  nosupbnd1lem2  27662  noinfbnd1lem2  27677  tghilberti2  28462  cvmlift2lem10  34955  btwnconn1lem1  35716  lplnexllnN  39069  2llnjN  39072  4atlem12b  39116  lplncvrlvol2  39120  lncmp  39288  cdlema2N  39297  cdleme11a  39765  cdleme24  39857  cdleme28  39878  cdlemefr29bpre0N  39911  cdlemefr29clN  39912  cdlemefr32fvaN  39914  cdlemefr32fva1  39915  cdlemefs29bpre0N  39921  cdlemefs29bpre1N  39922  cdlemefs29cpre1N  39923  cdlemefs29clN  39924  cdlemefs32fvaN  39927  cdlemefs32fva1  39928  cdleme36m  39966  cdleme17d3  40001  cdlemg36  40219  cdlemj3  40328  cdlemkid1  40427  cdlemk19ylem  40435  cdlemk19xlem  40447  dihlsscpre  40739  dihord4  40763  dihmeetlem1N  40795  dihatlat  40839  jm2.27  42460
  Copyright terms: Public domain W3C validator