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

Theorem simp22l 1074
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 981 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant2 977 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ax5seglem6  24634  segconeu  24706  3atlem2  30295  lplncvrlvol2  30426  paddasslem15  30645  4atex  30887  trlval4  30999  cdlemc5  31006  cdlemc6  31007  cdlemd2  31010  cdlemd3  31011  cdlemd4  31012  cdleme0moN  31036  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme11g  31076  cdleme11h  31077  cdleme11j  31078  cdleme11k  31079  cdleme11l  31080  cdleme11  31081  cdleme14  31084  cdleme15a  31085  cdleme15c  31087  cdleme15d  31088  cdleme15  31089  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme18a  31102  cdleme18b  31103  cdleme18c  31104  cdleme19b  31115  cdleme19e  31118  cdleme20bN  31121  cdleme20c  31122  cdleme20d  31123  cdleme20e  31124  cdleme20f  31125  cdleme20g  31126  cdleme20h  31127  cdleme20j  31129  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme21ct  31140  cdleme22d  31154  cdleme22e  31155  cdleme22eALTN  31156  cdleme26e  31170  cdleme27a  31178  cdleme28a  31181  cdleme30a  31189  cdleme43fsv1snlem  31231  cdlemefs44  31237  cdlemefs45ee  31241  cdleme35sn2aw  31269  cdleme36a  31271  cdleme39n  31277  cdleme40m  31278  cdleme42k  31295  cdlemeg47rv2  31321  cdlemeg46frv  31336  cdlemeg46vrg  31338  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemg2fv2  31411  cdlemg4g  31427  cdlemg4  31428  cdlemg6c  31431  cdlemg8b  31439  cdlemg8c  31440  cdlemg9a  31443  cdlemg9b  31444  cdlemg9  31445  cdlemg12a  31454  cdlemg12b  31455  cdlemg12c  31456  cdlemg17h  31479  cdlemg18b  31490  cdlemg18c  31491  cdlemg31b0a  31506  cdlemg27b  31507  cdlemg31d  31511  cdlemg28b  31514  cdlemg33a  31517  cdlemg33b  31518  cdlemg33c  31519  cdlemg33d  31520  cdlemg33e  31521  cdlemg33  31522  cdlemh  31628  cdlemk6  31648  cdlemki  31652  cdlemksat  31657  cdlemksv2  31658  cdlemk7  31659  cdlemk11  31660  cdlemk12  31661  cdlemkole  31664  cdlemk14  31665  cdlemk15  31666  cdlemk17  31669  cdlemk1u  31670  cdlemk5u  31672  cdlemk6u  31673  cdlemk7u  31681  cdlemk11u  31682  cdlemk12u  31683  cdlemk7u-2N  31699  cdlemk11u-2N  31700  cdlemk12u-2N  31701  cdlemk20-2N  31703  cdlemk28-3  31719  cdlemk33N  31720  cdlemk34  31721  cdlemk37  31725  cdlemk39  31727  cdlemk35s  31748  cdlemk39s  31750  cdlemk47  31760  cdlemk48  31761  cdlemk50  31763  cdlemk51  31764  cdlemk52  31765  cdlemkyyN  31773  cdlemk43N  31774  cdlemn2  32007  cdlemn10  32018
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