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

Theorem simp22l 1149
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 1056 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant2 1052 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  ax5seglem6  25043  segconeu  30849  3atlem2  33120  lplncvrlvol2  33251  paddasslem15  33470  4atex  33712  trlval4  33825  cdlemc5  33832  cdlemc6  33833  cdlemd2  33836  cdlemd3  33837  cdlemd4  33838  cdleme0moN  33862  cdleme3g  33871  cdleme3h  33872  cdleme3  33874  cdleme11g  33902  cdleme11h  33903  cdleme11j  33904  cdleme11k  33905  cdleme11l  33906  cdleme11  33907  cdleme14  33910  cdleme15a  33911  cdleme15c  33913  cdleme15d  33914  cdleme15  33915  cdleme16b  33916  cdleme16c  33917  cdleme16d  33918  cdleme16e  33919  cdleme16f  33920  cdleme18a  33928  cdleme18b  33929  cdleme18c  33930  cdleme19b  33942  cdleme19e  33945  cdleme20bN  33948  cdleme20c  33949  cdleme20d  33950  cdleme20e  33951  cdleme20f  33952  cdleme20g  33953  cdleme20h  33954  cdleme20j  33956  cdleme20l2  33959  cdleme20l  33960  cdleme20m  33961  cdleme21ct  33967  cdleme22d  33981  cdleme22e  33982  cdleme22eALTN  33983  cdleme26e  33997  cdleme27a  34005  cdleme28a  34008  cdleme30a  34016  cdleme43fsv1snlem  34058  cdlemefs44  34064  cdlemefs45ee  34068  cdleme35sn2aw  34096  cdleme36a  34098  cdleme39n  34104  cdleme40m  34105  cdleme42k  34122  cdlemeg47rv2  34148  cdlemeg46frv  34163  cdlemeg46vrg  34165  cdlemeg46rgv  34166  cdlemeg46req  34167  cdlemg2fv2  34238  cdlemg4g  34254  cdlemg4  34255  cdlemg6c  34258  cdlemg8b  34266  cdlemg8c  34267  cdlemg9a  34270  cdlemg9b  34271  cdlemg9  34272  cdlemg12a  34281  cdlemg12b  34282  cdlemg12c  34283  cdlemg17h  34306  cdlemg18b  34317  cdlemg18c  34318  cdlemg31b0a  34333  cdlemg27b  34334  cdlemg31d  34338  cdlemg28b  34341  cdlemg33a  34344  cdlemg33b  34345  cdlemg33c  34346  cdlemg33d  34347  cdlemg33e  34348  cdlemg33  34349  cdlemh  34455  cdlemk6  34475  cdlemki  34479  cdlemksat  34484  cdlemksv2  34485  cdlemk7  34486  cdlemk11  34487  cdlemk12  34488  cdlemkole  34491  cdlemk14  34492  cdlemk15  34493  cdlemk17  34496  cdlemk1u  34497  cdlemk5u  34499  cdlemk6u  34500  cdlemk7u  34508  cdlemk11u  34509  cdlemk12u  34510  cdlemk7u-2N  34526  cdlemk11u-2N  34527  cdlemk12u-2N  34528  cdlemk20-2N  34530  cdlemk28-3  34546  cdlemk33N  34547  cdlemk34  34548  cdlemk37  34552  cdlemk39  34554  cdlemk35s  34575  cdlemk39s  34577  cdlemk47  34587  cdlemk48  34588  cdlemk50  34590  cdlemk51  34591  cdlemk52  34592  cdlemkyyN  34600  cdlemk43N  34601  cdlemn2  34834  cdlemn10  34845
  Copyright terms: Public domain W3C validator