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

Theorem simp22l 1113
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp22l  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ph )

Proof of Theorem simp22l
StepHypRef Expression
1 simp2l 1020 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant2 1016 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  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  24439  segconeu  29889  3atlem2  35605  lplncvrlvol2  35736  paddasslem15  35955  4atex  36197  trlval4  36310  cdlemc5  36317  cdlemc6  36318  cdlemd2  36321  cdlemd3  36322  cdlemd4  36323  cdleme0moN  36347  cdleme3g  36356  cdleme3h  36357  cdleme3  36359  cdleme11g  36387  cdleme11h  36388  cdleme11j  36389  cdleme11k  36390  cdleme11l  36391  cdleme11  36392  cdleme14  36395  cdleme15a  36396  cdleme15c  36398  cdleme15d  36399  cdleme15  36400  cdleme16b  36401  cdleme16c  36402  cdleme16d  36403  cdleme16e  36404  cdleme16f  36405  cdleme18a  36413  cdleme18b  36414  cdleme18c  36415  cdleme19b  36427  cdleme19e  36430  cdleme20bN  36433  cdleme20c  36434  cdleme20d  36435  cdleme20e  36436  cdleme20f  36437  cdleme20g  36438  cdleme20h  36439  cdleme20j  36441  cdleme20l2  36444  cdleme20l  36445  cdleme20m  36446  cdleme21ct  36452  cdleme22d  36466  cdleme22e  36467  cdleme22eALTN  36468  cdleme26e  36482  cdleme27a  36490  cdleme28a  36493  cdleme30a  36501  cdleme43fsv1snlem  36543  cdlemefs44  36549  cdlemefs45ee  36553  cdleme35sn2aw  36581  cdleme36a  36583  cdleme39n  36589  cdleme40m  36590  cdleme42k  36607  cdlemeg47rv2  36633  cdlemeg46frv  36648  cdlemeg46vrg  36650  cdlemeg46rgv  36651  cdlemeg46req  36652  cdlemg2fv2  36723  cdlemg4g  36739  cdlemg4  36740  cdlemg6c  36743  cdlemg8b  36751  cdlemg8c  36752  cdlemg9a  36755  cdlemg9b  36756  cdlemg9  36757  cdlemg12a  36766  cdlemg12b  36767  cdlemg12c  36768  cdlemg17h  36791  cdlemg18b  36802  cdlemg18c  36803  cdlemg31b0a  36818  cdlemg27b  36819  cdlemg31d  36823  cdlemg28b  36826  cdlemg33a  36829  cdlemg33b  36830  cdlemg33c  36831  cdlemg33d  36832  cdlemg33e  36833  cdlemg33  36834  cdlemh  36940  cdlemk6  36960  cdlemki  36964  cdlemksat  36969  cdlemksv2  36970  cdlemk7  36971  cdlemk11  36972  cdlemk12  36973  cdlemkole  36976  cdlemk14  36977  cdlemk15  36978  cdlemk17  36981  cdlemk1u  36982  cdlemk5u  36984  cdlemk6u  36985  cdlemk7u  36993  cdlemk11u  36994  cdlemk12u  36995  cdlemk7u-2N  37011  cdlemk11u-2N  37012  cdlemk12u-2N  37013  cdlemk20-2N  37015  cdlemk28-3  37031  cdlemk33N  37032  cdlemk34  37033  cdlemk37  37037  cdlemk39  37039  cdlemk35s  37060  cdlemk39s  37062  cdlemk47  37072  cdlemk48  37073  cdlemk50  37075  cdlemk51  37076  cdlemk52  37077  cdlemkyyN  37085  cdlemk43N  37086  cdlemn2  37319  cdlemn10  37330
  Copyright terms: Public domain W3C validator