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

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

Proof of Theorem simp2ll
StepHypRef Expression
1 simpll 731 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant2 979 1  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  omeu  6820  4sqlem18  13322  vdwlem10  13350  0catg  13904  mvrf1  16481  tsmsxp  18176  ax5seglem3  25862  btwnconn1lem1  26013  btwnconn1lem2  26014  btwnconn1lem3  26015  btwnconn1lem12  26024  btwnconn1lem13  26025  pellex  26889  expmordi  27001  lshpkrlem6  29850  athgt  30190  2llnjN  30301  dalaw  30620  lhpmcvr4N  30760  cdlemb2  30775  4atexlemex6  30808  cdlemd7  30938  cdleme01N  30955  cdleme02N  30956  cdleme0ex1N  30957  cdleme0ex2N  30958  cdleme7aa  30976  cdleme7c  30979  cdleme7d  30980  cdleme7e  30981  cdleme7ga  30982  cdleme7  30983  cdleme11a  30994  cdleme20k  31053  cdleme27cl  31100  cdleme42e  31213  cdleme42h  31216  cdleme42i  31217  cdlemf  31297  cdlemg2kq  31336  cdlemg2m  31338  cdlemg8a  31361  cdlemg11aq  31372  cdlemg10c  31373  cdlemg11b  31376  cdlemg17a  31395  cdlemg31b0N  31428  cdlemg31c  31433  cdlemg33c0  31436  cdlemg41  31452  cdlemh2  31550  cdlemn9  31940  dihglbcpreN  32035  dihmeetlem3N  32040  dihmeetlem13N  32054
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator