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

Theorem simp2ll 1022
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 730 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant2 977 1  |-  ( ( th  /\  ( (
ph  /\  ps )  /\  ch )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  omeu  6583  4sqlem18  13009  vdwlem10  13037  0catg  13589  mvrf1  16170  tsmsxp  17837  ax5seglem3  24559  btwnconn1lem1  24710  btwnconn1lem2  24711  btwnconn1lem3  24712  btwnconn1lem12  24721  btwnconn1lem13  24722  pellex  26920  expmordi  27032  lshpkrlem6  29305  athgt  29645  2llnjN  29756  dalaw  30075  lhpmcvr4N  30215  cdlemb2  30230  4atexlemex6  30263  cdlemd7  30393  cdleme01N  30410  cdleme02N  30411  cdleme0ex1N  30412  cdleme0ex2N  30413  cdleme7aa  30431  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme7  30438  cdleme11a  30449  cdleme20k  30508  cdleme27cl  30555  cdleme42e  30668  cdleme42h  30671  cdleme42i  30672  cdlemf  30752  cdlemg2kq  30791  cdlemg2m  30793  cdlemg8a  30816  cdlemg11aq  30827  cdlemg10c  30828  cdlemg11b  30831  cdlemg17a  30850  cdlemg31b0N  30883  cdlemg31c  30888  cdlemg33c0  30891  cdlemg41  30907  cdlemh2  31005  cdlemn9  31395  dihglbcpreN  31490  dihmeetlem3N  31495  dihmeetlem13N  31509
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator