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

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

Proof of Theorem simp22
StepHypRef Expression
1 simp2 956 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 977 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl22  1034  simpr22  1043  simp122  1088  simp222  1097  simp322  1106  elfiun  7199  cofsmo  7911  modexp  11252  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  cgrextend  24703  btwnxfr  24751  colinearxfr  24770  lineext  24771  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  linecom  24845  cmpmorass  26069  bisig0  26165  isig22  26168  bnj966  29292  eqlkr  29911  lshpkrlem5  29926  omlmod1i2N  30072  cvrnbtwn3  30088  cvrcmp2  30096  cvlexch2  30141  cvlexchb2  30143  cvlatexchb2  30147  cvlatexch1  30148  cvlatexch2  30149  cvlatexch3  30150  cvlsupr7  30160  cvlsupr8  30161  atnlej1  30190  atnlej2  30191  2llnneN  30220  cvratlem  30232  atcvrneN  30241  atlelt  30249  2atjm  30256  3noncolr2  30260  3noncolr1N  30261  hlatcon2  30263  3dimlem2  30270  3dim1  30278  3dim2  30279  1cvrat  30287  ps-1  30288  ps-2  30289  2atjlej  30290  hlatexch3N  30291  ps-2b  30293  3atlem1  30294  3atlem5  30298  3atlem6  30299  2atm  30338  ps-2c  30339  lplni2  30348  lplnri3N  30366  llncvrlpln2  30368  2atmat  30372  2llnm2N  30379  2llnm3N  30380  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  paddasslem16  30646  pmodlem1  30657  pmod2iN  30660  hlmod1i  30667  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  osumcllem7N  30773  osumcllem9N  30775  pl42lem1N  30790  4atexlemswapqr  30874  4atex2  30888  4atex2-0bOLDN  30890  trlval4  30999  cdlemc5  31006  cdlemc6  31007  cdlemd2  31010  cdlemd4  31012  cdlemd6  31014  cdleme00a  31020  cdleme0e  31028  cdleme4  31049  cdleme4a  31050  cdleme5  31051  cdleme9  31064  cdleme16aN  31070  cdleme11c  31072  cdleme11dN  31073  cdleme11e  31074  cdleme11g  31076  cdleme11h  31077  cdleme11j  31078  cdleme11k  31079  cdleme11l  31080  cdleme11  31081  cdleme12  31082  cdleme13  31083  cdleme14  31084  cdleme15a  31085  cdleme15c  31087  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme16e  31093  cdleme16f  31094  cdleme17d1  31100  cdleme0nex  31101  cdleme18a  31102  cdleme18b  31103  cdleme18c  31104  cdleme18d  31106  cdlemednpq  31110  cdlemednuN  31111  cdleme20zN  31112  cdleme20y  31113  cdleme19a  31114  cdleme19b  31115  cdleme19d  31117  cdleme19e  31118  cdleme20aN  31120  cdleme20d  31123  cdleme20f  31125  cdleme20g  31126  cdleme20i  31128  cdleme20j  31129  cdleme20l1  31131  cdleme20l2  31132  cdleme20l  31133  cdleme20m  31134  cdleme21b  31137  cdleme21c  31138  cdleme21e  31142  cdleme21j  31147  cdleme22aa  31150  cdleme22a  31151  cdleme22b  31152  cdleme22cN  31153  cdleme22d  31154  cdleme22e  31155  cdleme22eALTN  31156  cdleme22f  31157  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme27N  31180  cdleme28a  31181  cdleme28b  31182  cdleme30a  31189  cdlemefs31fv1  31235  cdleme32b  31253  cdleme32c  31254  cdleme32e  31256  cdleme35h  31267  cdleme36a  31271  cdleme36m  31272  cdleme41sn3aw  31285  cdleme41sn4aw  31286  cdleme41fva11  31288  cdleme42k  31295  cdleme43cN  31302  cdleme46f2g1  31305  cdlemeg46fjgN  31332  cdlemeg46fjv  31334  cdlemeg46frv  31336  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemeg46gfv  31341  cdleme50trn2a  31361  cdlemg4a  31419  cdlemg4d  31424  cdlemg4e  31425  cdlemg4f  31426  cdlemg8c  31440  cdlemg9a  31443  cdlemg9b  31444  cdlemg10a  31451  cdlemg10  31452  cdlemg12b  31455  cdlemg12f  31459  cdlemg12g  31460  cdlemg12  31461  cdlemg17dN  31474  cdlemg17dALTN  31475  cdlemg17e  31476  cdlemg17f  31477  cdlemg17g  31478  cdlemg17i  31480  cdlemg17ir  31481  cdlemg17pq  31483  cdlemg17bq  31484  cdlemg17iqN  31485  cdlemg17  31488  cdlemg18b  31490  cdlemg18c  31491  cdlemg18d  31492  cdlemg18  31493  cdlemg19  31495  cdlemg21  31497  cdlemg28a  31504  cdlemg31b0a  31506  cdlemg27b  31507  cdlemg33b0  31512  cdlemg28b  31514  cdlemg28  31515  cdlemg35  31524  cdlemg36  31525  cdlemg44a  31542  cdlemh  31628  cdlemi2  31630  cdlemj1  31632  tendocan  31635  cdlemk5a  31646  cdlemk5  31647  cdlemki  31652  cdlemkvcl  31653  cdlemk10  31654  cdlemksv2  31658  cdlemk7  31659  cdlemk11  31660  cdlemk12  31661  cdlemkoatnle  31662  cdlemk15  31666  cdlemk16a  31667  cdlemk16  31668  cdlemk1u  31670  cdlemk5u  31672  cdlemk6u  31673  cdlemk18  31679  cdlemk19  31680  cdlemk7u  31681  cdlemk11u  31682  cdlemk12u  31683  cdlemk21N  31684  cdlemk20  31685  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  cdlemk22  31704  cdlemk30  31705  cdlemkuel-3  31709  cdlemkuv2-3N  31710  cdlemk18-3N  31711  cdlemkfid1N  31732  cdlemkid1  31733  cdlemkfid3N  31736  cdlemky  31737  cdlemk11ta  31740  cdlemk47  31760  cdlemk48  31761  cdlemk49  31762  cdlemk50  31763  cdlemk51  31764  cdlemk52  31765  cdlemk53a  31766  cdlemk53  31768  cdlemk54  31769  cdlemk55a  31770  cdlemkyyN  31773  cdlemk43N  31774  cdlemk55u1  31776  cdlemk55u  31777  cdlemk39u1  31778  cdlemk19u1  31780  cdleml1N  31787  cdleml2N  31788  cdleml3N  31789  dia2dimlem6  31881  cdlemn2  32007  cdlemn2a  32008  cdlemn5pre  32012  cdlemn11a  32019  dihjustlem  32028  dihjust  32029  dihmeetlem15N  32133  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