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

Theorem simp21 988
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 955 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
213ad2ant2 977 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl21  1033  simpr21  1042  simp121  1087  simp221  1096  simp321  1105  omeulem1  6596  cofsmo  7911  axdc4lem  8097  0catg  13605  funcoppc  13765  funcres  13786  catcisolem  13954  1stfcl  13987  2ndfcl  13988  prfcl  13993  evlfcl  14012  curf1cl  14018  curfcl  14022  hofcl  14049  meetle  14150  mulgdirlem  14607  prdsxmetlem  17948  isosctrlem3  20136  isosctr  20137  amgmlem  20300  colinearalg  24610  ax5seglem6  24634  ax5seg  24638  axpasch  24641  axeuclidlem  24662  axeuclid  24663  cgrtr  24687  cgrtr3  24689  ofscom  24702  segconeq  24705  ifscgr  24739  btwnxfr  24751  colinearxfr  24770  lineext  24771  brofs2  24772  brifs2  24773  fscgr  24775  linecgr  24776  btwnconn1lem1  24782  btwnconn1lem2  24783  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem5  24786  btwnconn1lem6  24787  btwnconn1lem7  24788  seglecgr12im  24805  seglecgr12  24806  segletr  24809  broutsideof3  24821  outsideofeq  24825  lineunray  24842  lineelsb2  24843  linecom  24845  cmpmorass  26069  bisig0  26165  isig1a2  26166  bnj1128  29336  lshpkrlem5  29926  omlmod1i2N  30072  cvrnbtwn3  30088  cvrcmp  30095  cvrcmp2  30096  cvlexch2  30141  cvlexchb2  30143  cvlatexchb2  30147  cvlatexch2  30149  cvlatexch3  30150  cvlsupr7  30160  atnlej1  30190  atnlej2  30191  2llnneN  30220  cvratlem  30232  atcvrneN  30241  atcvrj1  30242  atlelt  30249  2atjm  30256  3noncolr2  30260  3noncolr1N  30261  3dimlem2  30270  3dim1  30278  3dim2  30279  1cvrat  30287  ps-1  30288  ps-2  30289  2atjlej  30290  hlatexch3N  30291  ps-2b  30293  3atlem1  30294  3atlem2  30295  3atlem5  30298  3atlem6  30299  llnle  30329  2atm  30338  ps-2c  30339  lplni2  30348  lplnle  30351  lplnnle2at  30352  lplnri3N  30366  llncvrlpln2  30368  2atmat  30372  2llnm2N  30379  2llnm4  30381  2llnmeqat  30382  lvolnle3at  30393  4atlem0ae  30405  4atlem0be  30406  4atlem3b  30409  4atlem9  30414  4atlem10a  30415  4atlem10  30417  4atlem11a  30418  4atlem12a  30421  4at2  30425  2lplnm2N  30432  lneq2at  30589  2llnma1b  30597  2llnma1  30598  2llnma3r  30599  2llnma2  30600  2llnma2rN  30601  cdlema1N  30602  paddasslem2  30632  paddasslem15  30645  paddasslem16  30646  pmodlem1  30657  pmodlem2  30658  pmod2iN  30660  hlmod1i  30667  atmod1i1m  30669  atmod2i1  30672  atmod2i2  30673  atmod3i1  30675  atmod3i2  30676  atmod4i1  30677  atmod4i2  30678  llnexchb2lem  30679  llnexch2N  30681  dalawlem3  30684  dalawlem4  30685  dalawlem5  30686  dalawlem6  30687  dalawlem7  30688  dalawlem8  30689  dalawlem9  30690  dalawlem11  30692  dalawlem12  30693  dalawlem13  30694  dalawlem15  30696  osumcllem9N  30775  pl42lem1N  30790  4atexlems  30863  4atex2  30888  4atex2-0bOLDN  30890  trlval4  30999  cdlemc5  31006  cdlemc6  31007  cdlemd2  31010  cdlemd4  31012  cdlemd6  31014  cdleme00a  31020  cdleme0e  31028  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme4  31049  cdleme4a  31050  cdleme5  31051  cdleme9  31064  cdleme16aN  31070  cdleme11c  31072  cdleme11e  31074  cdleme11g  31076  cdleme11h  31077  cdleme11j  31078  cdleme11k  31079  cdleme11l  31080  cdleme11  31081  cdleme12  31082  cdleme14  31084  cdleme15c  31087  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme0nex  31101  cdleme18a  31102  cdleme18c  31104  cdleme18d  31106  cdlemednpq  31110  cdlemednuN  31111  cdleme20zN  31112  cdleme20y  31113  cdleme19a  31114  cdleme19b  31115  cdleme19d  31117  cdleme19e  31118  cdleme20aN  31120  cdleme20bN  31121  cdleme20c  31122  cdleme20d  31123  cdleme20f  31125  cdleme20g  31126  cdleme20i  31128  cdleme20j  31129  cdleme20l1  31131  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme21b  31137  cdleme21c  31138  cdleme21e  31142  cdleme21f  31143  cdleme22a  31151  cdleme22b  31152  cdleme22e  31155  cdleme22eALTN  31156  cdleme22f  31157  cdleme26eALTN  31172  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme27N  31180  cdleme28a  31181  cdleme28b  31182  cdleme30a  31189  cdleme43fsv1snlem  31231  cdlemefs31fv1  31235  cdlemefs45eN  31242  cdleme32b  31253  cdleme32c  31254  cdleme32d  31255  cdleme35h  31267  cdleme36a  31271  cdleme36m  31272  cdleme37m  31273  cdleme40m  31278  cdleme40n  31279  cdleme41sn3aw  31285  cdleme41sn4aw  31286  cdleme41fva11  31288  cdleme42k  31295  cdleme43cN  31302  cdleme43dN  31303  cdleme46f2g1  31305  cdlemeg47rv2  31321  cdlemeg46sfg  31331  cdlemeg46fjgN  31332  cdlemeg46rjgN  31333  cdlemeg46fjv  31334  cdlemeg46frv  31336  cdlemeg46vrg  31338  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemeg46gfv  31341  cdlemg4a  31419  cdlemg4d  31424  cdlemg4e  31425  cdlemg4f  31426  cdlemg4g  31427  cdlemg4  31428  cdlemg6d  31432  cdlemg6e  31433  cdlemg8b  31439  cdlemg8c  31440  cdlemg9a  31443  cdlemg9b  31444  cdlemg10a  31451  cdlemg10  31452  cdlemg12a  31454  cdlemg12b  31455  cdlemg12f  31459  cdlemg12g  31460  cdlemg12  31461  cdlemg17dN  31474  cdlemg17dALTN  31475  cdlemg17e  31476  cdlemg17f  31477  cdlemg17g  31478  cdlemg17h  31479  cdlemg17i  31480  cdlemg17pq  31483  cdlemg17iqN  31485  cdlemg17  31488  cdlemg18b  31490  cdlemg18c  31491  cdlemg19a  31494  cdlemg19  31495  cdlemg28a  31504  cdlemg27b  31507  cdlemg28b  31514  cdlemg28  31515  cdlemg33a  31517  cdlemg33b  31518  cdlemg33c  31519  cdlemg33d  31520  cdlemg33e  31521  cdlemg33  31522  cdlemg35  31524  cdlemg36  31525  cdlemg44a  31542  cdlemh  31628  cdlemi2  31630  cdlemj1  31632  tendocan  31635  cdlemk5a  31646  cdlemki  31652  cdlemkvcl  31653  cdlemk10  31654  cdlemksv2  31658  cdlemkole  31664  cdlemk14  31665  cdlemk15  31666  cdlemk16a  31667  cdlemk16  31668  cdlemk17  31669  cdlemk18  31679  cdlemk19  31680  cdlemkoatnle-2N  31686  cdlemk13-2N  31687  cdlemkole-2N  31688  cdlemk14-2N  31689  cdlemk15-2N  31690  cdlemk16-2N  31691  cdlemk17-2N  31692  cdlemk18-2N  31697  cdlemk19-2N  31698  cdlemk30  31705  cdlemk18-3N  31711  cdlemk23-3  31713  cdlemk25-3  31715  cdlemk27-3  31718  cdlemk37  31725  cdlemkfid1N  31732  cdlemkid1  31733  cdlemky  31737  cdlemk11ta  31740  cdlemk47  31760  cdlemk48  31761  cdlemk49  31762  cdlemk50  31763  cdlemk51  31764  cdlemk52  31765  cdlemk53a  31766  cdlemk54  31769  cdlemk39u1  31778  cdlemk19u1  31780  cdleml1N  31787  cdleml2N  31788  cdleml3N  31789  dia2dimlem6  31881  cdlemn2  32007  cdlemn2a  32008  cdlemn5pre  32012  cdlemn10  32018  cdlemn11c  32021  cdlemn11pre  32022  dihjustlem  32028  dihjust  32029  lclkrlem2y  32343
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator