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  23148  lshpkrlem5  32652  lplnexllnN  33101  4atexlemt  33590  4atex2  33614  4atex3  33618  trlval4  33725  cdlemc5  33732  cdlemc6  33733  cdlemd2  33736  cdleme0e  33754  cdleme0moN  33762  cdleme3g  33771  cdleme3h  33772  cdleme3  33774  cdleme4  33775  cdleme5  33777  cdleme9  33790  cdleme11fN  33801  cdleme11j  33804  cdleme11k  33805  cdleme11l  33806  cdleme11  33807  cdleme14  33810  cdleme15a  33811  cdleme15b  33812  cdleme15c  33813  cdleme16b  33816  cdleme16c  33817  cdleme16d  33818  cdleme16e  33819  cdleme16f  33820  cdleme17d1  33826  cdleme18c  33830  cdlemednpq  33836  cdleme19c  33842  cdleme20bN  33847  cdleme20d  33849  cdleme20f  33851  cdleme20g  33852  cdleme20h  33853  cdleme20j  33855  cdleme20l2  33858  cdleme20l  33859  cdleme20m  33860  cdleme22cN  33879  cdleme22d  33880  cdleme22e  33881  cdleme22f  33883  cdleme26fALTN  33899  cdleme26f  33900  cdleme26f2ALTN  33901  cdleme26f2  33902  cdleme27a  33904  cdleme28a  33907  cdlemefs44  33963  cdlemefs45ee  33967  cdleme32b  33979  cdleme32c  33980  cdleme32e  33982  cdleme35sn2aw  33995  cdleme37m  33999  cdleme39n  34003  cdleme40n  34005  cdleme40w  34007  cdleme42k  34021  cdlemeg47rv2  34047  cdlemeg46rjgN  34059  cdlemeg46rgv  34065  cdlemeg46req  34066  cdlemg2fv2  34137  cdlemg17h  34205  cdlemg31b0a  34232  cdlemg27b  34233  cdlemg31d  34237  cdlemg28b  34240  cdlemg28  34241  cdlemg29  34242  cdlemg33a  34243  cdlemg33b  34244  cdlemg33c  34245  cdlemg33d  34246  cdlemg33e  34247  cdlemg44a  34268  cdlemk7u-2N  34425  cdlemk11u-2N  34426  cdlemk12u-2N  34427  cdlemk26-3  34443  cdlemk27-3  34444  cdlemkfid3N  34462  cdlemn2  34733  cdlemn10  34744  cdlemn11c  34747
  Copyright terms: Public domain W3C validator