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

Theorem simp23l 1109
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 1016 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant2 1010 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  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:  ax5seglem6  23331  lshpkrlem5  33082  lplnexllnN  33531  4atexlemt  34020  4atex2  34044  4atex3  34048  trlval4  34155  cdlemc5  34162  cdlemc6  34163  cdlemd2  34166  cdleme0e  34184  cdleme0moN  34192  cdleme3g  34201  cdleme3h  34202  cdleme3  34204  cdleme4  34205  cdleme5  34207  cdleme9  34220  cdleme11fN  34231  cdleme11j  34234  cdleme11k  34235  cdleme11l  34236  cdleme11  34237  cdleme14  34240  cdleme15a  34241  cdleme15b  34242  cdleme15c  34243  cdleme16b  34246  cdleme16c  34247  cdleme16d  34248  cdleme16e  34249  cdleme16f  34250  cdleme17d1  34256  cdleme18c  34260  cdlemednpq  34266  cdleme19c  34272  cdleme20bN  34277  cdleme20d  34279  cdleme20f  34281  cdleme20g  34282  cdleme20h  34283  cdleme20j  34285  cdleme20l2  34288  cdleme20l  34289  cdleme20m  34290  cdleme22cN  34309  cdleme22d  34310  cdleme22e  34311  cdleme22f  34313  cdleme26fALTN  34329  cdleme26f  34330  cdleme26f2ALTN  34331  cdleme26f2  34332  cdleme27a  34334  cdleme28a  34337  cdlemefs44  34393  cdlemefs45ee  34397  cdleme32b  34409  cdleme32c  34410  cdleme32e  34412  cdleme35sn2aw  34425  cdleme37m  34429  cdleme39n  34433  cdleme40n  34435  cdleme40w  34437  cdleme42k  34451  cdlemeg47rv2  34477  cdlemeg46rjgN  34489  cdlemeg46rgv  34495  cdlemeg46req  34496  cdlemg2fv2  34567  cdlemg17h  34635  cdlemg31b0a  34662  cdlemg27b  34663  cdlemg31d  34667  cdlemg28b  34670  cdlemg28  34671  cdlemg29  34672  cdlemg33a  34673  cdlemg33b  34674  cdlemg33c  34675  cdlemg33d  34676  cdlemg33e  34677  cdlemg44a  34698  cdlemk7u-2N  34855  cdlemk11u-2N  34856  cdlemk12u-2N  34857  cdlemk26-3  34873  cdlemk27-3  34874  cdlemkfid3N  34892  cdlemn2  35163  cdlemn10  35174  cdlemn11c  35177
  Copyright terms: Public domain W3C validator