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

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

Proof of Theorem simp32l
StepHypRef Expression
1 simp2l 1023 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant3 1020 1  |-  ( ( ta  /\  et  /\  ( ch  /\  ( ph  /\  ps )  /\  th ) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 976
This theorem is referenced by:  cdlema1N  35255  paddasslem15  35298  4atex2-0aOLDN  35542  4atex3  35545  trlval3  35652  cdleme12  35736  cdleme19b  35770  cdleme19d  35772  cdleme19e  35773  cdleme20d  35778  cdleme20f  35780  cdleme20g  35781  cdleme21d  35796  cdleme21e  35797  cdleme21f  35798  cdleme22cN  35808  cdleme22e  35810  cdleme22f2  35813  cdleme22g  35814  cdleme26e  35825  cdleme28a  35836  cdleme37m  35928  cdleme39n  35932  cdlemg28b  36169  cdlemk3  36299  cdlemk12  36316  cdlemk12u  36338  cdlemkoatnle-2N  36341  cdlemk13-2N  36342  cdlemkole-2N  36343  cdlemk14-2N  36344  cdlemk15-2N  36345  cdlemk16-2N  36346  cdlemk17-2N  36347  cdlemk18-2N  36352  cdlemk19-2N  36353  cdlemk7u-2N  36354  cdlemk11u-2N  36355  cdlemk20-2N  36358  cdlemk30  36360  cdlemk23-3  36368  cdlemk24-3  36369
  Copyright terms: Public domain W3C validator