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  29717  cdlema1N  29980  trlval3  30376  cdleme12  30460  cdlemednpq  30488  cdleme19d  30495  cdleme19e  30496  cdleme20f  30503  cdleme20h  30505  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme21j  30525  cdleme22a  30529  cdleme22cN  30531  cdleme22f2  30536  cdleme32b  30631  cdlemg12f  30837  cdlemg12g  30838  cdlemg12  30839  cdlemg28a  30882  cdlemg31b0N  30883  cdlemg29  30894  cdlemg33a  30895  cdlemg36  30903  cdlemg42  30918  cdlemk16a  31045  cdlemk21-2N  31080  cdlemk32  31086  cdlemkid2  31113  cdlemk54  31147  cdlemk55a  31148  dihord10  31413
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