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

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

Proof of Theorem simp3lr
StepHypRef Expression
1 simplr 767 . 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:  f1oiso2  7366  omeu  8617  ntrivcvgmul  15908  tsmsxp  24153  tgqioo  24810  ovolunlem2  25521  plyadd  26247  plymul  26248  coeeu  26255  nosupbnd1lem2  27742  noinfbnd1lem2  27757  tghilberti2  28568  btwnconn1lem2  35914  btwnconn1lem3  35915  btwnconn1lem4  35916  athgt  39157  2llnjN  39268  4atlem12b  39312  lncmp  39484  cdlema2N  39493  cdleme21ct  40030  cdleme24  40053  cdleme27a  40068  cdleme28  40074  cdleme42b  40179  cdlemf  40264  dihlsscpre  40935  dihord4  40959  dihord5apre  40963  pellex  42510  jm2.27  42684
  Copyright terms: Public domain W3C validator