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  6599  4sqlem18  13025  vdwlem10  13053  0catg  13605  mvrf1  16186  tsmsxp  17853  ax5seglem3  24631  btwnconn1lem1  24782  btwnconn1lem2  24783  btwnconn1lem3  24784  btwnconn1lem12  24793  btwnconn1lem13  24794  pellex  27023  expmordi  27135  lshpkrlem6  29927  athgt  30267  2llnjN  30378  dalaw  30697  lhpmcvr4N  30837  cdlemb2  30852  4atexlemex6  30885  cdlemd7  31015  cdleme01N  31032  cdleme02N  31033  cdleme0ex1N  31034  cdleme0ex2N  31035  cdleme7aa  31053  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme7  31060  cdleme11a  31071  cdleme20k  31130  cdleme27cl  31177  cdleme42e  31290  cdleme42h  31293  cdleme42i  31294  cdlemf  31374  cdlemg2kq  31413  cdlemg2m  31415  cdlemg8a  31438  cdlemg11aq  31449  cdlemg10c  31450  cdlemg11b  31453  cdlemg17a  31472  cdlemg31b0N  31505  cdlemg31c  31510  cdlemg33c0  31513  cdlemg41  31529  cdlemh2  31627  cdlemn9  32017  dihglbcpreN  32112  dihmeetlem3N  32117  dihmeetlem13N  32131
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