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

Theorem simp31l 1119
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 1020 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant3 1019 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  ps-2c  34324  cdlema1N  34587  trlval3  34983  cdleme12  35067  cdlemednpq  35095  cdleme19d  35102  cdleme19e  35103  cdleme20f  35110  cdleme20h  35112  cdleme20l2  35117  cdleme20l  35118  cdleme20m  35119  cdleme21j  35132  cdleme22a  35136  cdleme22cN  35138  cdleme22f2  35143  cdleme32b  35238  cdlemg12f  35444  cdlemg12g  35445  cdlemg12  35446  cdlemg28a  35489  cdlemg31b0N  35490  cdlemg29  35501  cdlemg33a  35502  cdlemg36  35510  cdlemg42  35525  cdlemk16a  35652  cdlemk21-2N  35687  cdlemk32  35693  cdlemkid2  35720  cdlemk54  35754  cdlemk55a  35755  dihord10  36020
  Copyright terms: Public domain W3C validator