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

Theorem simp31l 1078
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 979 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant3 978 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ps-2c  30339  cdlema1N  30602  trlval3  30998  cdleme12  31082  cdlemednpq  31110  cdleme19d  31117  cdleme19e  31118  cdleme20f  31125  cdleme20h  31127  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme21j  31147  cdleme22a  31151  cdleme22cN  31153  cdleme22f2  31158  cdleme32b  31253  cdlemg12f  31459  cdlemg12g  31460  cdlemg12  31461  cdlemg28a  31504  cdlemg31b0N  31505  cdlemg29  31516  cdlemg33a  31517  cdlemg36  31525  cdlemg42  31540  cdlemk16a  31667  cdlemk21-2N  31702  cdlemk32  31708  cdlemkid2  31735  cdlemk54  31769  cdlemk55a  31770  dihord10  32035
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