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  26879  expmordi  26991  lshpkrlem6  29840  athgt  30180  2llnjN  30291  dalaw  30610  lhpmcvr4N  30750  cdlemb2  30765  4atexlemex6  30798  cdlemd7  30928  cdleme01N  30945  cdleme02N  30946  cdleme0ex1N  30947  cdleme0ex2N  30948  cdleme7aa  30966  cdleme7c  30969  cdleme7d  30970  cdleme7e  30971  cdleme7ga  30972  cdleme7  30973  cdleme11a  30984  cdleme20k  31043  cdleme27cl  31090  cdleme42e  31203  cdleme42h  31206  cdleme42i  31207  cdlemf  31287  cdlemg2kq  31326  cdlemg2m  31328  cdlemg8a  31351  cdlemg11aq  31362  cdlemg10c  31363  cdlemg11b  31366  cdlemg17a  31385  cdlemg31b0N  31418  cdlemg31c  31423  cdlemg33c0  31426  cdlemg41  31442  cdlemh2  31540  cdlemn9  31930  dihglbcpreN  32025  dihmeetlem3N  32030  dihmeetlem13N  32044
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