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 768 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜓)
213ad2ant3 1132 1 ((𝜃𝜏 ∧ ((𝜑𝜓) ∧ 𝜒)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  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 210  df-an 400  df-3an 1086
This theorem is referenced by:  f1oiso2  7088  omeu  8198  ntrivcvgmul  15253  tsmsxp  22763  tgqioo  23408  ovolunlem2  24105  plyadd  24817  plymul  24818  coeeu  24825  tghilberti2  26435  nosupbnd1lem2  33317  btwnconn1lem2  33657  btwnconn1lem3  33658  btwnconn1lem4  33659  athgt  36745  2llnjN  36856  4atlem12b  36900  lncmp  37072  cdlema2N  37081  cdleme21ct  37618  cdleme24  37641  cdleme27a  37656  cdleme28  37662  cdleme42b  37767  cdlemf  37852  dihlsscpre  38523  dihord4  38547  dihord5apre  38551  pellex  39763  jm2.27  39936
  Copyright terms: Public domain W3C validator