MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp23l 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  25777  lshpkrlem5  29597  lplnexllnN  30046  4atexlemt  30535  4atex2  30559  4atex3  30563  trlval4  30670  cdlemc5  30677  cdlemc6  30678  cdlemd2  30681  cdleme0e  30699  cdleme0moN  30707  cdleme3g  30716  cdleme3h  30717  cdleme3  30719  cdleme4  30720  cdleme5  30722  cdleme9  30735  cdleme11fN  30746  cdleme11j  30749  cdleme11k  30750  cdleme11l  30751  cdleme11  30752  cdleme14  30755  cdleme15a  30756  cdleme15b  30757  cdleme15c  30758  cdleme16b  30761  cdleme16c  30762  cdleme16d  30763  cdleme16e  30764  cdleme16f  30765  cdleme17d1  30771  cdleme18c  30775  cdlemednpq  30781  cdleme19c  30787  cdleme20bN  30792  cdleme20d  30794  cdleme20f  30796  cdleme20g  30797  cdleme20h  30798  cdleme20j  30800  cdleme20l2  30803  cdleme20l  30804  cdleme20m  30805  cdleme22cN  30824  cdleme22d  30825  cdleme22e  30826  cdleme22f  30828  cdleme26fALTN  30844  cdleme26f  30845  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme27a  30849  cdleme28a  30852  cdlemefs44  30908  cdlemefs45ee  30912  cdleme32b  30924  cdleme32c  30925  cdleme32e  30927  cdleme35sn2aw  30940  cdleme37m  30944  cdleme39n  30948  cdleme40n  30950  cdleme40w  30952  cdleme42k  30966  cdlemeg47rv2  30992  cdlemeg46rjgN  31004  cdlemeg46rgv  31010  cdlemeg46req  31011  cdlemg2fv2  31082  cdlemg17h  31150  cdlemg31b0a  31177  cdlemg27b  31178  cdlemg31d  31182  cdlemg28b  31185  cdlemg28  31186  cdlemg29  31187  cdlemg33a  31188  cdlemg33b  31189  cdlemg33c  31190  cdlemg33d  31191  cdlemg33e  31192  cdlemg44a  31213  cdlemk7u-2N  31370  cdlemk11u-2N  31371  cdlemk12u-2N  31372  cdlemk26-3  31388  cdlemk27-3  31389  cdlemkfid3N  31407  cdlemn2  31678  cdlemn10  31689  cdlemn11c  31692
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