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  24562  segconeu  24634  3atlem2  29673  lplncvrlvol2  29804  paddasslem15  30023  4atex  30265  trlval4  30377  cdlemc5  30384  cdlemc6  30385  cdlemd2  30388  cdlemd3  30389  cdlemd4  30390  cdleme0moN  30414  cdleme3g  30423  cdleme3h  30424  cdleme3  30426  cdleme11g  30454  cdleme11h  30455  cdleme11j  30456  cdleme11k  30457  cdleme11l  30458  cdleme11  30459  cdleme14  30462  cdleme15a  30463  cdleme15c  30465  cdleme15d  30466  cdleme15  30467  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme18a  30480  cdleme18b  30481  cdleme18c  30482  cdleme19b  30493  cdleme19e  30496  cdleme20bN  30499  cdleme20c  30500  cdleme20d  30501  cdleme20e  30502  cdleme20f  30503  cdleme20g  30504  cdleme20h  30505  cdleme20j  30507  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme21ct  30518  cdleme22d  30532  cdleme22e  30533  cdleme22eALTN  30534  cdleme26e  30548  cdleme27a  30556  cdleme28a  30559  cdleme30a  30567  cdleme43fsv1snlem  30609  cdlemefs44  30615  cdlemefs45ee  30619  cdleme35sn2aw  30647  cdleme36a  30649  cdleme39n  30655  cdleme40m  30656  cdleme42k  30673  cdlemeg47rv2  30699  cdlemeg46frv  30714  cdlemeg46vrg  30716  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemg2fv2  30789  cdlemg4g  30805  cdlemg4  30806  cdlemg6c  30809  cdlemg8b  30817  cdlemg8c  30818  cdlemg9a  30821  cdlemg9b  30822  cdlemg9  30823  cdlemg12a  30832  cdlemg12b  30833  cdlemg12c  30834  cdlemg17h  30857  cdlemg18b  30868  cdlemg18c  30869  cdlemg31b0a  30884  cdlemg27b  30885  cdlemg31d  30889  cdlemg28b  30892  cdlemg33a  30895  cdlemg33b  30896  cdlemg33c  30897  cdlemg33d  30898  cdlemg33e  30899  cdlemg33  30900  cdlemh  31006  cdlemk6  31026  cdlemki  31030  cdlemksat  31035  cdlemksv2  31036  cdlemk7  31037  cdlemk11  31038  cdlemk12  31039  cdlemkole  31042  cdlemk14  31043  cdlemk15  31044  cdlemk17  31047  cdlemk1u  31048  cdlemk5u  31050  cdlemk6u  31051  cdlemk7u  31059  cdlemk11u  31060  cdlemk12u  31061  cdlemk7u-2N  31077  cdlemk11u-2N  31078  cdlemk12u-2N  31079  cdlemk20-2N  31081  cdlemk28-3  31097  cdlemk33N  31098  cdlemk34  31099  cdlemk37  31103  cdlemk39  31105  cdlemk35s  31126  cdlemk39s  31128  cdlemk47  31138  cdlemk48  31139  cdlemk50  31141  cdlemk51  31142  cdlemk52  31143  cdlemkyyN  31151  cdlemk43N  31152  cdlemn2  31385  cdlemn10  31396
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