MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2ll 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  6764  4sqlem18  13257  vdwlem10  13285  0catg  13839  mvrf1  16416  tsmsxp  18105  ax5seglem3  25584  btwnconn1lem1  25735  btwnconn1lem2  25736  btwnconn1lem3  25737  btwnconn1lem12  25746  btwnconn1lem13  25747  pellex  26589  expmordi  26701  lshpkrlem6  29230  athgt  29570  2llnjN  29681  dalaw  30000  lhpmcvr4N  30140  cdlemb2  30155  4atexlemex6  30188  cdlemd7  30318  cdleme01N  30335  cdleme02N  30336  cdleme0ex1N  30337  cdleme0ex2N  30338  cdleme7aa  30356  cdleme7c  30359  cdleme7d  30360  cdleme7e  30361  cdleme7ga  30362  cdleme7  30363  cdleme11a  30374  cdleme20k  30433  cdleme27cl  30480  cdleme42e  30593  cdleme42h  30596  cdleme42i  30597  cdlemf  30677  cdlemg2kq  30716  cdlemg2m  30718  cdlemg8a  30741  cdlemg11aq  30752  cdlemg10c  30753  cdlemg11b  30756  cdlemg17a  30775  cdlemg31b0N  30808  cdlemg31c  30813  cdlemg33c0  30816  cdlemg41  30832  cdlemh2  30930  cdlemn9  31320  dihglbcpreN  31415  dihmeetlem3N  31420  dihmeetlem13N  31434
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