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

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

Proof of Theorem simp3ll
StepHypRef Expression
1 simpll 763 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
213ad2ant3 1129 1 ((𝜃𝜏 ∧ ((𝜑𝜓) ∧ 𝜒)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  f1oiso2  7099  omeu  8206  ntrivcvgmul  15253  tsmsxp  22697  tgqioo  23342  ovolunlem2  24033  plyadd  24741  plymul  24742  coeeu  24749  tghilberti2  26357  nosupbnd1lem2  33112  btwnconn1lem2  33452  btwnconn1lem3  33453  btwnconn1lem12  33462  athgt  36478  2llnjN  36589  4atlem12b  36633  lncmp  36805  cdlema2N  36814  cdlemc2  37214  cdleme5  37262  cdleme11a  37282  cdleme21ct  37351  cdleme21  37359  cdleme22eALTN  37367  cdleme24  37374  cdleme27cl  37388  cdleme27a  37389  cdleme28  37395  cdleme36a  37482  cdleme42b  37500  cdleme48fvg  37522  cdlemf  37585  cdlemk39  37938  cdlemkid1  37944  dihlsscpre  38256  dihord4  38280  dihord5apre  38284  dihmeetlem20N  38348  mapdh9a  38811  pellex  39316  jm2.27  39489
  Copyright terms: Public domain W3C validator