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

Theorem simp22l 1115
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 1022 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant2 1018 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 371  df-3an 975
This theorem is referenced by:  ax5seglem6  24010  segconeu  29514  3atlem2  34497  lplncvrlvol2  34628  paddasslem15  34847  4atex  35089  trlval4  35201  cdlemc5  35208  cdlemc6  35209  cdlemd2  35212  cdlemd3  35213  cdlemd4  35214  cdleme0moN  35238  cdleme3g  35247  cdleme3h  35248  cdleme3  35250  cdleme11g  35278  cdleme11h  35279  cdleme11j  35280  cdleme11k  35281  cdleme11l  35282  cdleme11  35283  cdleme14  35286  cdleme15a  35287  cdleme15c  35289  cdleme15d  35290  cdleme15  35291  cdleme16b  35292  cdleme16c  35293  cdleme16d  35294  cdleme16e  35295  cdleme16f  35296  cdleme18a  35304  cdleme18b  35305  cdleme18c  35306  cdleme19b  35317  cdleme19e  35320  cdleme20bN  35323  cdleme20c  35324  cdleme20d  35325  cdleme20e  35326  cdleme20f  35327  cdleme20g  35328  cdleme20h  35329  cdleme20j  35331  cdleme20l2  35334  cdleme20l  35335  cdleme20m  35336  cdleme21ct  35342  cdleme22d  35356  cdleme22e  35357  cdleme22eALTN  35358  cdleme26e  35372  cdleme27a  35380  cdleme28a  35383  cdleme30a  35391  cdleme43fsv1snlem  35433  cdlemefs44  35439  cdlemefs45ee  35443  cdleme35sn2aw  35471  cdleme36a  35473  cdleme39n  35479  cdleme40m  35480  cdleme42k  35497  cdlemeg47rv2  35523  cdlemeg46frv  35538  cdlemeg46vrg  35540  cdlemeg46rgv  35541  cdlemeg46req  35542  cdlemg2fv2  35613  cdlemg4g  35629  cdlemg4  35630  cdlemg6c  35633  cdlemg8b  35641  cdlemg8c  35642  cdlemg9a  35645  cdlemg9b  35646  cdlemg9  35647  cdlemg12a  35656  cdlemg12b  35657  cdlemg12c  35658  cdlemg17h  35681  cdlemg18b  35692  cdlemg18c  35693  cdlemg31b0a  35708  cdlemg27b  35709  cdlemg31d  35713  cdlemg28b  35716  cdlemg33a  35719  cdlemg33b  35720  cdlemg33c  35721  cdlemg33d  35722  cdlemg33e  35723  cdlemg33  35724  cdlemh  35830  cdlemk6  35850  cdlemki  35854  cdlemksat  35859  cdlemksv2  35860  cdlemk7  35861  cdlemk11  35862  cdlemk12  35863  cdlemkole  35866  cdlemk14  35867  cdlemk15  35868  cdlemk17  35871  cdlemk1u  35872  cdlemk5u  35874  cdlemk6u  35875  cdlemk7u  35883  cdlemk11u  35884  cdlemk12u  35885  cdlemk7u-2N  35901  cdlemk11u-2N  35902  cdlemk12u-2N  35903  cdlemk20-2N  35905  cdlemk28-3  35921  cdlemk33N  35922  cdlemk34  35923  cdlemk37  35927  cdlemk39  35929  cdlemk35s  35950  cdlemk39s  35952  cdlemk47  35962  cdlemk48  35963  cdlemk50  35965  cdlemk51  35966  cdlemk52  35967  cdlemkyyN  35975  cdlemk43N  35976  cdlemn2  36209  cdlemn10  36220
  Copyright terms: Public domain W3C validator