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

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

Proof of Theorem simp3ll
StepHypRef Expression
1 simpll 805 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
213ad2ant3 1104 1 ((𝜃𝜏 ∧ ((𝜑𝜓) ∧ 𝜒)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 1056
This theorem is referenced by:  f1oiso2  6642  omeu  7710  ntrivcvgmul  14678  tsmsxp  22005  tgqioo  22650  ovolunlem2  23312  plyadd  24018  plymul  24019  coeeu  24026  tghilberti2  25578  nosupbnd1lem2  31980  btwnconn1lem2  32320  btwnconn1lem3  32321  btwnconn1lem12  32330  athgt  35060  2llnjN  35171  4atlem12b  35215  lncmp  35387  cdlema2N  35396  cdlemc2  35797  cdleme5  35845  cdleme11a  35865  cdleme21ct  35934  cdleme21  35942  cdleme22eALTN  35950  cdleme24  35957  cdleme27cl  35971  cdleme27a  35972  cdleme28  35978  cdleme36a  36065  cdleme42b  36083  cdleme48fvg  36105  cdlemf  36168  cdlemk39  36521  cdlemkid1  36527  dihlsscpre  36840  dihord4  36864  dihord5apre  36868  dihmeetlem20N  36932  mapdh9a  37396  pellex  37716  jm2.27  37892
  Copyright terms: Public domain W3C validator