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

Theorem simp22l 1077
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 984 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
213ad2ant2 980 1  |-  ( ( ta  /\  ( ch 
/\  ( ph  /\  ps )  /\  th )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  ax5seglem6  25875  segconeu  25947  3atlem2  30283  lplncvrlvol2  30414  paddasslem15  30633  4atex  30875  trlval4  30987  cdlemc5  30994  cdlemc6  30995  cdlemd2  30998  cdlemd3  30999  cdlemd4  31000  cdleme0moN  31024  cdleme3g  31033  cdleme3h  31034  cdleme3  31036  cdleme11g  31064  cdleme11h  31065  cdleme11j  31066  cdleme11k  31067  cdleme11l  31068  cdleme11  31069  cdleme14  31072  cdleme15a  31073  cdleme15c  31075  cdleme15d  31076  cdleme15  31077  cdleme16b  31078  cdleme16c  31079  cdleme16d  31080  cdleme16e  31081  cdleme16f  31082  cdleme18a  31090  cdleme18b  31091  cdleme18c  31092  cdleme19b  31103  cdleme19e  31106  cdleme20bN  31109  cdleme20c  31110  cdleme20d  31111  cdleme20e  31112  cdleme20f  31113  cdleme20g  31114  cdleme20h  31115  cdleme20j  31117  cdleme20l2  31120  cdleme20l  31121  cdleme20m  31122  cdleme21ct  31128  cdleme22d  31142  cdleme22e  31143  cdleme22eALTN  31144  cdleme26e  31158  cdleme27a  31166  cdleme28a  31169  cdleme30a  31177  cdleme43fsv1snlem  31219  cdlemefs44  31225  cdlemefs45ee  31229  cdleme35sn2aw  31257  cdleme36a  31259  cdleme39n  31265  cdleme40m  31266  cdleme42k  31283  cdlemeg47rv2  31309  cdlemeg46frv  31324  cdlemeg46vrg  31326  cdlemeg46rgv  31327  cdlemeg46req  31328  cdlemg2fv2  31399  cdlemg4g  31415  cdlemg4  31416  cdlemg6c  31419  cdlemg8b  31427  cdlemg8c  31428  cdlemg9a  31431  cdlemg9b  31432  cdlemg9  31433  cdlemg12a  31442  cdlemg12b  31443  cdlemg12c  31444  cdlemg17h  31467  cdlemg18b  31478  cdlemg18c  31479  cdlemg31b0a  31494  cdlemg27b  31495  cdlemg31d  31499  cdlemg28b  31502  cdlemg33a  31505  cdlemg33b  31506  cdlemg33c  31507  cdlemg33d  31508  cdlemg33e  31509  cdlemg33  31510  cdlemh  31616  cdlemk6  31636  cdlemki  31640  cdlemksat  31645  cdlemksv2  31646  cdlemk7  31647  cdlemk11  31648  cdlemk12  31649  cdlemkole  31652  cdlemk14  31653  cdlemk15  31654  cdlemk17  31657  cdlemk1u  31658  cdlemk5u  31660  cdlemk6u  31661  cdlemk7u  31669  cdlemk11u  31670  cdlemk12u  31671  cdlemk7u-2N  31687  cdlemk11u-2N  31688  cdlemk12u-2N  31689  cdlemk20-2N  31691  cdlemk28-3  31707  cdlemk33N  31708  cdlemk34  31709  cdlemk37  31713  cdlemk39  31715  cdlemk35s  31736  cdlemk39s  31738  cdlemk47  31748  cdlemk48  31749  cdlemk50  31751  cdlemk51  31752  cdlemk52  31753  cdlemkyyN  31761  cdlemk43N  31762  cdlemn2  31995  cdlemn10  32006
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator