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

Theorem simp21 990
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp21  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ps )

Proof of Theorem simp21
StepHypRef Expression
1 simp1 957 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
213ad2ant2 979 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl21  1035  simpr21  1044  simp121  1089  simp221  1098  simp321  1107  omeulem1  6825  cofsmo  8149  axdc4lem  8335  0catg  13912  funcoppc  14072  funcres  14093  catcisolem  14261  1stfcl  14294  2ndfcl  14295  prfcl  14300  evlfcl  14319  curf1cl  14325  curfcl  14329  hofcl  14356  meetle  14457  mulgdirlem  14914  prdsxmetlem  18398  isosctrlem3  20664  isosctr  20665  amgmlem  20828  ofldaddlt  24241  rhmdvd  24259  colinearalg  25849  ax5seglem6  25873  ax5seg  25877  axpasch  25880  axeuclidlem  25901  axeuclid  25902  cgrtr  25926  cgrtr3  25928  ofscom  25941  segconeq  25944  ifscgr  25978  btwnxfr  25990  colinearxfr  26009  lineext  26010  brofs2  26011  brifs2  26012  fscgr  26014  linecgr  26015  btwnconn1lem1  26021  btwnconn1lem2  26022  btwnconn1lem3  26023  btwnconn1lem4  26024  btwnconn1lem5  26025  btwnconn1lem6  26026  btwnconn1lem7  26027  seglecgr12im  26044  seglecgr12  26045  segletr  26048  broutsideof3  26060  outsideofeq  26064  lineunray  26081  lineelsb2  26082  linecom  26084  bnj1128  29359  lshpkrlem5  29912  omlmod1i2N  30058  cvrnbtwn3  30074  cvrcmp  30081  cvrcmp2  30082  cvlexch2  30127  cvlexchb2  30129  cvlatexchb2  30133  cvlatexch2  30135  cvlatexch3  30136  cvlsupr7  30146  atnlej1  30176  atnlej2  30177  2llnneN  30206  cvratlem  30218  atcvrneN  30227  atcvrj1  30228  atlelt  30235  2atjm  30242  3noncolr2  30246  3noncolr1N  30247  3dimlem2  30256  3dim1  30264  3dim2  30265  1cvrat  30273  ps-1  30274  ps-2  30275  2atjlej  30276  hlatexch3N  30277  ps-2b  30279  3atlem1  30280  3atlem2  30281  3atlem5  30284  3atlem6  30285  llnle  30315  2atm  30324  ps-2c  30325  lplni2  30334  lplnle  30337  lplnnle2at  30338  lplnri3N  30352  llncvrlpln2  30354  2atmat  30358  2llnm2N  30365  2llnm4  30367  2llnmeqat  30368  lvolnle3at  30379  4atlem0ae  30391  4atlem0be  30392  4atlem3b  30395  4atlem9  30400  4atlem10a  30401  4atlem10  30403  4atlem11a  30404  4atlem12a  30407  4at2  30411  2lplnm2N  30418  lneq2at  30575  2llnma1b  30583  2llnma1  30584  2llnma3r  30585  2llnma2  30586  2llnma2rN  30587  cdlema1N  30588  paddasslem2  30618  paddasslem15  30631  paddasslem16  30632  pmodlem1  30643  pmodlem2  30644  pmod2iN  30646  hlmod1i  30653  atmod1i1m  30655  atmod2i1  30658  atmod2i2  30659  atmod3i1  30661  atmod3i2  30662  atmod4i1  30663  atmod4i2  30664  llnexchb2lem  30665  llnexch2N  30667  dalawlem3  30670  dalawlem4  30671  dalawlem5  30672  dalawlem6  30673  dalawlem7  30674  dalawlem8  30675  dalawlem9  30676  dalawlem11  30678  dalawlem12  30679  dalawlem13  30680  dalawlem15  30682  osumcllem9N  30761  pl42lem1N  30776  4atexlems  30849  4atex2  30874  4atex2-0bOLDN  30876  trlval4  30985  cdlemc5  30992  cdlemc6  30993  cdlemd2  30996  cdlemd4  30998  cdlemd6  31000  cdleme00a  31006  cdleme0e  31014  cdleme3g  31031  cdleme3h  31032  cdleme3  31034  cdleme4  31035  cdleme4a  31036  cdleme5  31037  cdleme9  31050  cdleme16aN  31056  cdleme11c  31058  cdleme11e  31060  cdleme11g  31062  cdleme11h  31063  cdleme11j  31064  cdleme11k  31065  cdleme11l  31066  cdleme11  31067  cdleme12  31068  cdleme14  31070  cdleme15c  31073  cdleme16b  31076  cdleme16c  31077  cdleme16d  31078  cdleme16e  31079  cdleme16f  31080  cdleme0nex  31087  cdleme18a  31088  cdleme18c  31090  cdleme18d  31092  cdlemednpq  31096  cdlemednuN  31097  cdleme20zN  31098  cdleme20y  31099  cdleme19a  31100  cdleme19b  31101  cdleme19d  31103  cdleme19e  31104  cdleme20aN  31106  cdleme20bN  31107  cdleme20c  31108  cdleme20d  31109  cdleme20f  31111  cdleme20g  31112  cdleme20i  31114  cdleme20j  31115  cdleme20l1  31117  cdleme20l2  31118  cdleme20l  31119  cdleme20m  31120  cdleme21b  31123  cdleme21c  31124  cdleme21e  31128  cdleme21f  31129  cdleme22a  31137  cdleme22b  31138  cdleme22e  31141  cdleme22eALTN  31142  cdleme22f  31143  cdleme26eALTN  31158  cdleme26fALTN  31159  cdleme26f  31160  cdleme26f2ALTN  31161  cdleme26f2  31162  cdleme27N  31166  cdleme28a  31167  cdleme28b  31168  cdleme30a  31175  cdleme43fsv1snlem  31217  cdlemefs31fv1  31221  cdlemefs45eN  31228  cdleme32b  31239  cdleme32c  31240  cdleme32d  31241  cdleme35h  31253  cdleme36a  31257  cdleme36m  31258  cdleme37m  31259  cdleme40m  31264  cdleme40n  31265  cdleme41sn3aw  31271  cdleme41sn4aw  31272  cdleme41fva11  31274  cdleme42k  31281  cdleme43cN  31288  cdleme43dN  31289  cdleme46f2g1  31291  cdlemeg47rv2  31307  cdlemeg46sfg  31317  cdlemeg46fjgN  31318  cdlemeg46rjgN  31319  cdlemeg46fjv  31320  cdlemeg46frv  31322  cdlemeg46vrg  31324  cdlemeg46rgv  31325  cdlemeg46req  31326  cdlemeg46gfv  31327  cdlemg4a  31405  cdlemg4d  31410  cdlemg4e  31411  cdlemg4f  31412  cdlemg4g  31413  cdlemg4  31414  cdlemg6d  31418  cdlemg6e  31419  cdlemg8b  31425  cdlemg8c  31426  cdlemg9a  31429  cdlemg9b  31430  cdlemg10a  31437  cdlemg10  31438  cdlemg12a  31440  cdlemg12b  31441  cdlemg12f  31445  cdlemg12g  31446  cdlemg12  31447  cdlemg17dN  31460  cdlemg17dALTN  31461  cdlemg17e  31462  cdlemg17f  31463  cdlemg17g  31464  cdlemg17h  31465  cdlemg17i  31466  cdlemg17pq  31469  cdlemg17iqN  31471  cdlemg17  31474  cdlemg18b  31476  cdlemg18c  31477  cdlemg19a  31480  cdlemg19  31481  cdlemg28a  31490  cdlemg27b  31493  cdlemg28b  31500  cdlemg28  31501  cdlemg33a  31503  cdlemg33b  31504  cdlemg33c  31505  cdlemg33d  31506  cdlemg33e  31507  cdlemg33  31508  cdlemg35  31510  cdlemg36  31511  cdlemg44a  31528  cdlemh  31614  cdlemi2  31616  cdlemj1  31618  tendocan  31621  cdlemk5a  31632  cdlemki  31638  cdlemkvcl  31639  cdlemk10  31640  cdlemksv2  31644  cdlemkole  31650  cdlemk14  31651  cdlemk15  31652  cdlemk16a  31653  cdlemk16  31654  cdlemk17  31655  cdlemk18  31665  cdlemk19  31666  cdlemkoatnle-2N  31672  cdlemk13-2N  31673  cdlemkole-2N  31674  cdlemk14-2N  31675  cdlemk15-2N  31676  cdlemk16-2N  31677  cdlemk17-2N  31678  cdlemk18-2N  31683  cdlemk19-2N  31684  cdlemk30  31691  cdlemk18-3N  31697  cdlemk23-3  31699  cdlemk25-3  31701  cdlemk27-3  31704  cdlemk37  31711  cdlemkfid1N  31718  cdlemkid1  31719  cdlemky  31723  cdlemk11ta  31726  cdlemk47  31746  cdlemk48  31747  cdlemk49  31748  cdlemk50  31749  cdlemk51  31750  cdlemk52  31751  cdlemk53a  31752  cdlemk54  31755  cdlemk39u1  31764  cdlemk19u1  31766  cdleml1N  31773  cdleml2N  31774  cdleml3N  31775  dia2dimlem6  31867  cdlemn2  31993  cdlemn2a  31994  cdlemn5pre  31998  cdlemn10  32004  cdlemn11c  32007  cdlemn11pre  32008  dihjustlem  32014  dihjust  32015  lclkrlem2y  32329
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator