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

Theorem simp31l 1080
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp31l  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ph )

Proof of Theorem simp31l
StepHypRef Expression
1 simp1l 981 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant3 980 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ps-2c  29643  cdlema1N  29906  trlval3  30302  cdleme12  30386  cdlemednpq  30414  cdleme19d  30421  cdleme19e  30422  cdleme20f  30429  cdleme20h  30431  cdleme20l2  30436  cdleme20l  30437  cdleme20m  30438  cdleme21j  30451  cdleme22a  30455  cdleme22cN  30457  cdleme22f2  30462  cdleme32b  30557  cdlemg12f  30763  cdlemg12g  30764  cdlemg12  30765  cdlemg28a  30808  cdlemg31b0N  30809  cdlemg29  30820  cdlemg33a  30821  cdlemg36  30829  cdlemg42  30844  cdlemk16a  30971  cdlemk21-2N  31006  cdlemk32  31012  cdlemkid2  31039  cdlemk54  31073  cdlemk55a  31074  dihord10  31339
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