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

Theorem simp3ll 1029
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp3ll  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ph )

Proof of Theorem simp3ll
StepHypRef Expression
1 simpll 732 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant3 981 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  f1oiso2  6101  omeu  6857  tsmsxp  18215  tgqioo  18862  ovolunlem2  19425  plyadd  20167  plymul  20168  coeeu  20175  ntrivcvgmul  25261  btwnconn1lem2  26053  btwnconn1lem3  26054  btwnconn1lem12  26063  pellex  26936  jm2.27  27117  athgt  30351  2llnjN  30462  4atlem12b  30506  lncmp  30678  cdlema2N  30687  cdlemc2  31087  cdleme5  31135  cdleme11a  31155  cdleme21ct  31224  cdleme21  31232  cdleme22eALTN  31240  cdleme24  31247  cdleme27cl  31261  cdleme27a  31262  cdleme28  31268  cdleme36a  31355  cdleme42b  31373  cdleme48fvg  31395  cdlemf  31458  cdlemk39  31811  cdlemkid1  31817  dihlsscpre  32130  dihord4  32154  dihord5apre  32158  dihmeetlem20N  32222  mapdh9a  32686
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator