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

Theorem simp23l 1076
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 983 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant2 977 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ax5seglem6  24562  lshpkrlem5  29304  lplnexllnN  29753  4atexlemt  30242  4atex2  30266  4atex3  30270  trlval4  30377  cdlemc5  30384  cdlemc6  30385  cdlemd2  30388  cdleme0e  30406  cdleme0moN  30414  cdleme3g  30423  cdleme3h  30424  cdleme3  30426  cdleme4  30427  cdleme5  30429  cdleme9  30442  cdleme11fN  30453  cdleme11j  30456  cdleme11k  30457  cdleme11l  30458  cdleme11  30459  cdleme14  30462  cdleme15a  30463  cdleme15b  30464  cdleme15c  30465  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme17d1  30478  cdleme18c  30482  cdlemednpq  30488  cdleme19c  30494  cdleme20bN  30499  cdleme20d  30501  cdleme20f  30503  cdleme20g  30504  cdleme20h  30505  cdleme20j  30507  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme22cN  30531  cdleme22d  30532  cdleme22e  30533  cdleme22f  30535  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme27a  30556  cdleme28a  30559  cdlemefs44  30615  cdlemefs45ee  30619  cdleme32b  30631  cdleme32c  30632  cdleme32e  30634  cdleme35sn2aw  30647  cdleme37m  30651  cdleme39n  30655  cdleme40n  30657  cdleme40w  30659  cdleme42k  30673  cdlemeg47rv2  30699  cdlemeg46rjgN  30711  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemg2fv2  30789  cdlemg17h  30857  cdlemg31b0a  30884  cdlemg27b  30885  cdlemg31d  30889  cdlemg28b  30892  cdlemg28  30893  cdlemg29  30894  cdlemg33a  30895  cdlemg33b  30896  cdlemg33c  30897  cdlemg33d  30898  cdlemg33e  30899  cdlemg44a  30920  cdlemk7u-2N  31077  cdlemk11u-2N  31078  cdlemk12u-2N  31079  cdlemk26-3  31095  cdlemk27-3  31096  cdlemkfid3N  31114  cdlemn2  31385  cdlemn10  31396  cdlemn11c  31399
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator