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

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

Proof of Theorem simp3ll
StepHypRef Expression
1 simpll 807 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
213ad2ant3 1130 1 ((𝜃𝜏 ∧ ((𝜑𝜓) ∧ 𝜒)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  f1oiso2  6765  omeu  7834  ntrivcvgmul  14833  tsmsxp  22159  tgqioo  22804  ovolunlem2  23466  plyadd  24172  plymul  24173  coeeu  24180  tghilberti2  25732  nosupbnd1lem2  32161  btwnconn1lem2  32501  btwnconn1lem3  32502  btwnconn1lem12  32511  athgt  35245  2llnjN  35356  4atlem12b  35400  lncmp  35572  cdlema2N  35581  cdlemc2  35982  cdleme5  36030  cdleme11a  36050  cdleme21ct  36119  cdleme21  36127  cdleme22eALTN  36135  cdleme24  36142  cdleme27cl  36156  cdleme27a  36157  cdleme28  36163  cdleme36a  36250  cdleme42b  36268  cdleme48fvg  36290  cdlemf  36353  cdlemk39  36706  cdlemkid1  36712  dihlsscpre  37025  dihord4  37049  dihord5apre  37053  dihmeetlem20N  37117  mapdh9a  37581  pellex  37901  jm2.27  38077
  Copyright terms: Public domain W3C validator