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

Theorem simp22l 1107
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 1014 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant2 1010 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  ax5seglem6  23202  segconeu  28064  3atlem2  33224  lplncvrlvol2  33355  paddasslem15  33574  4atex  33816  trlval4  33928  cdlemc5  33935  cdlemc6  33936  cdlemd2  33939  cdlemd3  33940  cdlemd4  33941  cdleme0moN  33965  cdleme3g  33974  cdleme3h  33975  cdleme3  33977  cdleme11g  34005  cdleme11h  34006  cdleme11j  34007  cdleme11k  34008  cdleme11l  34009  cdleme11  34010  cdleme14  34013  cdleme15a  34014  cdleme15c  34016  cdleme15d  34017  cdleme15  34018  cdleme16b  34019  cdleme16c  34020  cdleme16d  34021  cdleme16e  34022  cdleme16f  34023  cdleme18a  34031  cdleme18b  34032  cdleme18c  34033  cdleme19b  34044  cdleme19e  34047  cdleme20bN  34050  cdleme20c  34051  cdleme20d  34052  cdleme20e  34053  cdleme20f  34054  cdleme20g  34055  cdleme20h  34056  cdleme20j  34058  cdleme20l2  34061  cdleme20l  34062  cdleme20m  34063  cdleme21ct  34069  cdleme22d  34083  cdleme22e  34084  cdleme22eALTN  34085  cdleme26e  34099  cdleme27a  34107  cdleme28a  34110  cdleme30a  34118  cdleme43fsv1snlem  34160  cdlemefs44  34166  cdlemefs45ee  34170  cdleme35sn2aw  34198  cdleme36a  34200  cdleme39n  34206  cdleme40m  34207  cdleme42k  34224  cdlemeg47rv2  34250  cdlemeg46frv  34265  cdlemeg46vrg  34267  cdlemeg46rgv  34268  cdlemeg46req  34269  cdlemg2fv2  34340  cdlemg4g  34356  cdlemg4  34357  cdlemg6c  34360  cdlemg8b  34368  cdlemg8c  34369  cdlemg9a  34372  cdlemg9b  34373  cdlemg9  34374  cdlemg12a  34383  cdlemg12b  34384  cdlemg12c  34385  cdlemg17h  34408  cdlemg18b  34419  cdlemg18c  34420  cdlemg31b0a  34435  cdlemg27b  34436  cdlemg31d  34440  cdlemg28b  34443  cdlemg33a  34446  cdlemg33b  34447  cdlemg33c  34448  cdlemg33d  34449  cdlemg33e  34450  cdlemg33  34451  cdlemh  34557  cdlemk6  34577  cdlemki  34581  cdlemksat  34586  cdlemksv2  34587  cdlemk7  34588  cdlemk11  34589  cdlemk12  34590  cdlemkole  34593  cdlemk14  34594  cdlemk15  34595  cdlemk17  34598  cdlemk1u  34599  cdlemk5u  34601  cdlemk6u  34602  cdlemk7u  34610  cdlemk11u  34611  cdlemk12u  34612  cdlemk7u-2N  34628  cdlemk11u-2N  34629  cdlemk12u-2N  34630  cdlemk20-2N  34632  cdlemk28-3  34648  cdlemk33N  34649  cdlemk34  34650  cdlemk37  34654  cdlemk39  34656  cdlemk35s  34677  cdlemk39s  34679  cdlemk47  34689  cdlemk48  34690  cdlemk50  34692  cdlemk51  34693  cdlemk52  34694  cdlemkyyN  34702  cdlemk43N  34703  cdlemn2  34936  cdlemn10  34947
  Copyright terms: Public domain W3C validator