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

Theorem simp3ll 1236
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 1127 1 ((𝜃𝜏 ∧ ((𝜑𝜓) ∧ 𝜒)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 1081
This theorem is referenced by:  f1oiso2  7094  omeu  8201  ntrivcvgmul  15248  tsmsxp  22692  tgqioo  23337  ovolunlem2  24028  plyadd  24736  plymul  24737  coeeu  24744  tghilberti2  26352  nosupbnd1lem2  33107  btwnconn1lem2  33447  btwnconn1lem3  33448  btwnconn1lem12  33457  athgt  36474  2llnjN  36585  4atlem12b  36629  lncmp  36801  cdlema2N  36810  cdlemc2  37210  cdleme5  37258  cdleme11a  37278  cdleme21ct  37347  cdleme21  37355  cdleme22eALTN  37363  cdleme24  37370  cdleme27cl  37384  cdleme27a  37385  cdleme28  37391  cdleme36a  37478  cdleme42b  37496  cdleme48fvg  37518  cdlemf  37581  cdlemk39  37934  cdlemkid1  37940  dihlsscpre  38252  dihord4  38276  dihord5apre  38280  dihmeetlem20N  38344  mapdh9a  38807  pellex  39312  jm2.27  39485
  Copyright terms: Public domain W3C validator