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

Theorem simp22l 1125
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 1032 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant2 1028 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  ax5seglem6  24956  segconeu  30777  3atlem2  32974  lplncvrlvol2  33105  paddasslem15  33324  4atex  33566  trlval4  33679  cdlemc5  33686  cdlemc6  33687  cdlemd2  33690  cdlemd3  33691  cdlemd4  33692  cdleme0moN  33716  cdleme3g  33725  cdleme3h  33726  cdleme3  33728  cdleme11g  33756  cdleme11h  33757  cdleme11j  33758  cdleme11k  33759  cdleme11l  33760  cdleme11  33761  cdleme14  33764  cdleme15a  33765  cdleme15c  33767  cdleme15d  33768  cdleme15  33769  cdleme16b  33770  cdleme16c  33771  cdleme16d  33772  cdleme16e  33773  cdleme16f  33774  cdleme18a  33782  cdleme18b  33783  cdleme18c  33784  cdleme19b  33796  cdleme19e  33799  cdleme20bN  33802  cdleme20c  33803  cdleme20d  33804  cdleme20e  33805  cdleme20f  33806  cdleme20g  33807  cdleme20h  33808  cdleme20j  33810  cdleme20l2  33813  cdleme20l  33814  cdleme20m  33815  cdleme21ct  33821  cdleme22d  33835  cdleme22e  33836  cdleme22eALTN  33837  cdleme26e  33851  cdleme27a  33859  cdleme28a  33862  cdleme30a  33870  cdleme43fsv1snlem  33912  cdlemefs44  33918  cdlemefs45ee  33922  cdleme35sn2aw  33950  cdleme36a  33952  cdleme39n  33958  cdleme40m  33959  cdleme42k  33976  cdlemeg47rv2  34002  cdlemeg46frv  34017  cdlemeg46vrg  34019  cdlemeg46rgv  34020  cdlemeg46req  34021  cdlemg2fv2  34092  cdlemg4g  34108  cdlemg4  34109  cdlemg6c  34112  cdlemg8b  34120  cdlemg8c  34121  cdlemg9a  34124  cdlemg9b  34125  cdlemg9  34126  cdlemg12a  34135  cdlemg12b  34136  cdlemg12c  34137  cdlemg17h  34160  cdlemg18b  34171  cdlemg18c  34172  cdlemg31b0a  34187  cdlemg27b  34188  cdlemg31d  34192  cdlemg28b  34195  cdlemg33a  34198  cdlemg33b  34199  cdlemg33c  34200  cdlemg33d  34201  cdlemg33e  34202  cdlemg33  34203  cdlemh  34309  cdlemk6  34329  cdlemki  34333  cdlemksat  34338  cdlemksv2  34339  cdlemk7  34340  cdlemk11  34341  cdlemk12  34342  cdlemkole  34345  cdlemk14  34346  cdlemk15  34347  cdlemk17  34350  cdlemk1u  34351  cdlemk5u  34353  cdlemk6u  34354  cdlemk7u  34362  cdlemk11u  34363  cdlemk12u  34364  cdlemk7u-2N  34380  cdlemk11u-2N  34381  cdlemk12u-2N  34382  cdlemk20-2N  34384  cdlemk28-3  34400  cdlemk33N  34401  cdlemk34  34402  cdlemk37  34406  cdlemk39  34408  cdlemk35s  34429  cdlemk39s  34431  cdlemk47  34441  cdlemk48  34442  cdlemk50  34444  cdlemk51  34445  cdlemk52  34446  cdlemkyyN  34454  cdlemk43N  34455  cdlemn2  34688  cdlemn10  34699
  Copyright terms: Public domain W3C validator