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

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

Proof of Theorem simp3ll
StepHypRef Expression
1 simpll 767 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜑)
213ad2ant3 1136 1 ((𝜃𝜏 ∧ ((𝜑𝜓) ∧ 𝜒)) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1088
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 210  df-an 400  df-3an 1090
This theorem is referenced by:  f1oiso2  7131  omeu  8255  ntrivcvgmul  15363  tsmsxp  22919  tgqioo  23565  ovolunlem2  24263  plyadd  24979  plymul  24980  coeeu  24987  tghilberti2  26597  nosupbnd1lem2  33568  noinfbnd1lem2  33583  btwnconn1lem2  34046  btwnconn1lem3  34047  btwnconn1lem12  34056  athgt  37126  2llnjN  37237  4atlem12b  37281  lncmp  37453  cdlema2N  37462  cdlemc2  37862  cdleme5  37910  cdleme11a  37930  cdleme21ct  37999  cdleme21  38007  cdleme22eALTN  38015  cdleme24  38022  cdleme27cl  38036  cdleme27a  38037  cdleme28  38043  cdleme36a  38130  cdleme42b  38148  cdleme48fvg  38170  cdlemf  38233  cdlemk39  38586  cdlemkid1  38592  dihlsscpre  38904  dihord4  38928  dihord5apre  38932  dihmeetlem20N  38996  mapdh9a  39459  pellex  40270  jm2.27  40443
  Copyright terms: Public domain W3C validator