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

Theorem simp31l 1080
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 981 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant3 980 1  |-  ( ( ta  /\  et  /\  ( ( ph  /\  ps )  /\  ch  /\  th ) )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ps-2c  30010  cdlema1N  30273  trlval3  30669  cdleme12  30753  cdlemednpq  30781  cdleme19d  30788  cdleme19e  30789  cdleme20f  30796  cdleme20h  30798  cdleme20l2  30803  cdleme20l  30804  cdleme20m  30805  cdleme21j  30818  cdleme22a  30822  cdleme22cN  30824  cdleme22f2  30829  cdleme32b  30924  cdlemg12f  31130  cdlemg12g  31131  cdlemg12  31132  cdlemg28a  31175  cdlemg31b0N  31176  cdlemg29  31187  cdlemg33a  31188  cdlemg36  31196  cdlemg42  31211  cdlemk16a  31338  cdlemk21-2N  31373  cdlemk32  31379  cdlemkid2  31406  cdlemk54  31440  cdlemk55a  31441  dihord10  31706
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator