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

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

Proof of Theorem simp23l
StepHypRef Expression
1 simp3l 985 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant2 979 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ax5seglem6  25873  lshpkrlem5  29912  lplnexllnN  30361  4atexlemt  30850  4atex2  30874  4atex3  30878  trlval4  30985  cdlemc5  30992  cdlemc6  30993  cdlemd2  30996  cdleme0e  31014  cdleme0moN  31022  cdleme3g  31031  cdleme3h  31032  cdleme3  31034  cdleme4  31035  cdleme5  31037  cdleme9  31050  cdleme11fN  31061  cdleme11j  31064  cdleme11k  31065  cdleme11l  31066  cdleme11  31067  cdleme14  31070  cdleme15a  31071  cdleme15b  31072  cdleme15c  31073  cdleme16b  31076  cdleme16c  31077  cdleme16d  31078  cdleme16e  31079  cdleme16f  31080  cdleme17d1  31086  cdleme18c  31090  cdlemednpq  31096  cdleme19c  31102  cdleme20bN  31107  cdleme20d  31109  cdleme20f  31111  cdleme20g  31112  cdleme20h  31113  cdleme20j  31115  cdleme20l2  31118  cdleme20l  31119  cdleme20m  31120  cdleme22cN  31139  cdleme22d  31140  cdleme22e  31141  cdleme22f  31143  cdleme26fALTN  31159  cdleme26f  31160  cdleme26f2ALTN  31161  cdleme26f2  31162  cdleme27a  31164  cdleme28a  31167  cdlemefs44  31223  cdlemefs45ee  31227  cdleme32b  31239  cdleme32c  31240  cdleme32e  31242  cdleme35sn2aw  31255  cdleme37m  31259  cdleme39n  31263  cdleme40n  31265  cdleme40w  31267  cdleme42k  31281  cdlemeg47rv2  31307  cdlemeg46rjgN  31319  cdlemeg46rgv  31325  cdlemeg46req  31326  cdlemg2fv2  31397  cdlemg17h  31465  cdlemg31b0a  31492  cdlemg27b  31493  cdlemg31d  31497  cdlemg28b  31500  cdlemg28  31501  cdlemg29  31502  cdlemg33a  31503  cdlemg33b  31504  cdlemg33c  31505  cdlemg33d  31506  cdlemg33e  31507  cdlemg44a  31528  cdlemk7u-2N  31685  cdlemk11u-2N  31686  cdlemk12u-2N  31687  cdlemk26-3  31703  cdlemk27-3  31704  cdlemkfid3N  31722  cdlemn2  31993  cdlemn10  32004  cdlemn11c  32007
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