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

Theorem simp32l 1113
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 1014 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant3 1011 1  |-  ( ( ta  /\  et  /\  ( ch  /\  ( ph  /\  ps )  /\  th ) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  cdlema1N  33432  paddasslem15  33475  4atex2-0aOLDN  33719  4atex3  33722  trlval3  33828  cdleme12  33912  cdleme19b  33945  cdleme19d  33947  cdleme19e  33948  cdleme20d  33953  cdleme20f  33955  cdleme20g  33956  cdleme21d  33971  cdleme21e  33972  cdleme21f  33973  cdleme22cN  33983  cdleme22e  33985  cdleme22f2  33988  cdleme22g  33989  cdleme26e  34000  cdleme28a  34011  cdleme37m  34103  cdleme39n  34107  cdlemg28b  34344  cdlemk3  34474  cdlemk12  34491  cdlemk12u  34513  cdlemkoatnle-2N  34516  cdlemk13-2N  34517  cdlemkole-2N  34518  cdlemk14-2N  34519  cdlemk15-2N  34520  cdlemk16-2N  34521  cdlemk17-2N  34522  cdlemk18-2N  34527  cdlemk19-2N  34528  cdlemk7u-2N  34529  cdlemk11u-2N  34530  cdlemk20-2N  34533  cdlemk30  34535  cdlemk23-3  34543  cdlemk24-3  34544
  Copyright terms: Public domain W3C validator