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

Theorem simp32l 1116
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 1017 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant3 1014 1  |-  ( ( ta  /\  et  /\  ( ch  /\  ( ph  /\  ps )  /\  th ) )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 970
This theorem is referenced by:  cdlema1N  34462  paddasslem15  34505  4atex2-0aOLDN  34749  4atex3  34752  trlval3  34858  cdleme12  34942  cdleme19b  34975  cdleme19d  34977  cdleme19e  34978  cdleme20d  34983  cdleme20f  34985  cdleme20g  34986  cdleme21d  35001  cdleme21e  35002  cdleme21f  35003  cdleme22cN  35013  cdleme22e  35015  cdleme22f2  35018  cdleme22g  35019  cdleme26e  35030  cdleme28a  35041  cdleme37m  35133  cdleme39n  35137  cdlemg28b  35374  cdlemk3  35504  cdlemk12  35521  cdlemk12u  35543  cdlemkoatnle-2N  35546  cdlemk13-2N  35547  cdlemkole-2N  35548  cdlemk14-2N  35549  cdlemk15-2N  35550  cdlemk16-2N  35551  cdlemk17-2N  35552  cdlemk18-2N  35557  cdlemk19-2N  35558  cdlemk7u-2N  35559  cdlemk11u-2N  35560  cdlemk20-2N  35563  cdlemk30  35565  cdlemk23-3  35573  cdlemk24-3  35574
  Copyright terms: Public domain W3C validator