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

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

Proof of Theorem simp3ll
StepHypRef Expression
1 simpll 774 . 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:  f1oiso2  6823  omeu  7899  ntrivcvgmul  14851  tsmsxp  22167  tgqioo  22812  ovolunlem2  23475  plyadd  24183  plymul  24184  coeeu  24191  tghilberti2  25743  nosupbnd1lem2  32173  btwnconn1lem2  32513  btwnconn1lem3  32514  btwnconn1lem12  32523  athgt  35233  2llnjN  35344  4atlem12b  35388  lncmp  35560  cdlema2N  35569  cdlemc2  35970  cdleme5  36018  cdleme11a  36038  cdleme21ct  36107  cdleme21  36115  cdleme22eALTN  36123  cdleme24  36130  cdleme27cl  36144  cdleme27a  36145  cdleme28  36151  cdleme36a  36238  cdleme42b  36256  cdleme48fvg  36278  cdlemf  36341  cdlemk39  36694  cdlemkid1  36700  dihlsscpre  37012  dihord4  37036  dihord5apre  37040  dihmeetlem20N  37104  mapdh9a  37567  pellex  37898  jm2.27  38073
  Copyright terms: Public domain W3C validator