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  8200  ntrivcvgmul  15246  tsmsxp  22690  tgqioo  23335  ovolunlem2  24026  plyadd  24734  plymul  24735  coeeu  24742  tghilberti2  26351  nosupbnd1lem2  33106  btwnconn1lem2  33446  btwnconn1lem3  33447  btwnconn1lem12  33456  athgt  36472  2llnjN  36583  4atlem12b  36627  lncmp  36799  cdlema2N  36808  cdlemc2  37208  cdleme5  37256  cdleme11a  37276  cdleme21ct  37345  cdleme21  37353  cdleme22eALTN  37361  cdleme24  37368  cdleme27cl  37382  cdleme27a  37383  cdleme28  37389  cdleme36a  37476  cdleme42b  37494  cdleme48fvg  37516  cdlemf  37579  cdlemk39  37932  cdlemkid1  37938  dihlsscpre  38250  dihord4  38274  dihord5apre  38278  dihmeetlem20N  38342  mapdh9a  38805  pellex  39310  jm2.27  39483
  Copyright terms: Public domain W3C validator