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

Theorem simp2ll 1025
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 732 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant2 980 1  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  omeu  6831  4sqlem18  13335  vdwlem10  13363  0catg  13917  mvrf1  16494  tsmsxp  18189  ax5seglem3  25875  btwnconn1lem1  26026  btwnconn1lem2  26027  btwnconn1lem3  26028  btwnconn1lem12  26037  btwnconn1lem13  26038  pellex  26912  expmordi  27024  lshpkrlem6  29987  athgt  30327  2llnjN  30438  dalaw  30757  lhpmcvr4N  30897  cdlemb2  30912  4atexlemex6  30945  cdlemd7  31075  cdleme01N  31092  cdleme02N  31093  cdleme0ex1N  31094  cdleme0ex2N  31095  cdleme7aa  31113  cdleme7c  31116  cdleme7d  31117  cdleme7e  31118  cdleme7ga  31119  cdleme7  31120  cdleme11a  31131  cdleme20k  31190  cdleme27cl  31237  cdleme42e  31350  cdleme42h  31353  cdleme42i  31354  cdlemf  31434  cdlemg2kq  31473  cdlemg2m  31475  cdlemg8a  31498  cdlemg11aq  31509  cdlemg10c  31510  cdlemg11b  31513  cdlemg17a  31532  cdlemg31b0N  31565  cdlemg31c  31570  cdlemg33c0  31573  cdlemg41  31589  cdlemh2  31687  cdlemn9  32077  dihglbcpreN  32172  dihmeetlem3N  32177  dihmeetlem13N  32191
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