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

Theorem simp23l 1115
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 1022 . 2  |-  ( ( ch  /\  th  /\  ( ph  /\  ps )
)  ->  ph )
213ad2ant2 1016 1  |-  ( ( ta  /\  ( ch 
/\  th  /\  ( ph  /\  ps ) )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  ax5seglem6  24442  lshpkrlem5  35255  lplnexllnN  35704  4atexlemt  36193  4atex2  36217  4atex3  36221  trlval4  36329  cdlemc5  36336  cdlemc6  36337  cdlemd2  36340  cdleme0e  36358  cdleme0moN  36366  cdleme3g  36375  cdleme3h  36376  cdleme3  36378  cdleme4  36379  cdleme5  36381  cdleme9  36394  cdleme11fN  36405  cdleme11j  36408  cdleme11k  36409  cdleme11l  36410  cdleme11  36411  cdleme14  36414  cdleme15a  36415  cdleme15b  36416  cdleme15c  36417  cdleme16b  36420  cdleme16c  36421  cdleme16d  36422  cdleme16e  36423  cdleme16f  36424  cdleme17d1  36430  cdleme18c  36434  cdlemednpq  36440  cdleme19c  36447  cdleme20bN  36452  cdleme20d  36454  cdleme20f  36456  cdleme20g  36457  cdleme20h  36458  cdleme20j  36460  cdleme20l2  36463  cdleme20l  36464  cdleme20m  36465  cdleme22cN  36484  cdleme22d  36485  cdleme22e  36486  cdleme22f  36488  cdleme26fALTN  36504  cdleme26f  36505  cdleme26f2ALTN  36506  cdleme26f2  36507  cdleme27a  36509  cdleme28a  36512  cdlemefs44  36568  cdlemefs45ee  36572  cdleme32b  36584  cdleme32c  36585  cdleme32e  36587  cdleme35sn2aw  36600  cdleme37m  36604  cdleme39n  36608  cdleme40n  36610  cdleme40w  36612  cdleme42k  36626  cdlemeg47rv2  36652  cdlemeg46rjgN  36664  cdlemeg46rgv  36670  cdlemeg46req  36671  cdlemg2fv2  36742  cdlemg17h  36810  cdlemg31b0a  36837  cdlemg27b  36838  cdlemg31d  36842  cdlemg28b  36845  cdlemg28  36846  cdlemg29  36847  cdlemg33a  36848  cdlemg33b  36849  cdlemg33c  36850  cdlemg33d  36851  cdlemg33e  36852  cdlemg44a  36873  cdlemk7u-2N  37030  cdlemk11u-2N  37031  cdlemk12u-2N  37032  cdlemk26-3  37048  cdlemk27-3  37049  cdlemkfid3N  37067  cdlemn2  37338  cdlemn10  37349  cdlemn11c  37352
  Copyright terms: Public domain W3C validator