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

Theorem simp22 991
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 958 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 979 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl22  1036  simpr22  1045  simp122  1090  simp222  1099  simp322  1108  elfiun  7393  cofsmo  8105  modexp  11469  funcoppc  14027  funcres  14048  catcisolem  14216  1stfcl  14249  2ndfcl  14250  prfcl  14255  evlfcl  14274  curf1cl  14280  curfcl  14284  hofcl  14311  meetle  14412  mulgdirlem  14869  prdsxmetlem  18351  isosctrlem3  20617  isosctr  20618  amgmlem  20781  ofldaddlt  24194  rhmdvd  24212  colinearalg  25753  ax5seglem6  25777  ax5seg  25781  axpasch  25784  axeuclidlem  25805  axeuclid  25806  cgrtr  25830  cgrtr3  25832  ofscom  25845  cgrextend  25846  btwnxfr  25894  colinearxfr  25913  lineext  25914  fscgr  25918  linecgr  25919  btwnconn1lem1  25925  btwnconn1lem2  25926  btwnconn1lem3  25927  btwnconn1lem4  25928  btwnconn1lem5  25929  btwnconn1lem6  25930  btwnconn1lem7  25931  seglecgr12im  25948  seglecgr12  25949  segletr  25952  broutsideof3  25964  outsideofeq  25968  lineunray  25985  linecom  25988  bnj966  29021  eqlkr  29582  lshpkrlem5  29597  omlmod1i2N  29743  cvrnbtwn3  29759  cvrcmp2  29767  cvlexch2  29812  cvlexchb2  29814  cvlatexchb2  29818  cvlatexch1  29819  cvlatexch2  29820  cvlatexch3  29821  cvlsupr7  29831  cvlsupr8  29832  atnlej1  29861  atnlej2  29862  2llnneN  29891  cvratlem  29903  atcvrneN  29912  atlelt  29920  2atjm  29927  3noncolr2  29931  3noncolr1N  29932  hlatcon2  29934  3dimlem2  29941  3dim1  29949  3dim2  29950  1cvrat  29958  ps-1  29959  ps-2  29960  2atjlej  29961  hlatexch3N  29962  ps-2b  29964  3atlem1  29965  3atlem5  29969  3atlem6  29970  2atm  30009  ps-2c  30010  lplni2  30019  lplnri3N  30037  llncvrlpln2  30039  2atmat  30043  2llnm2N  30050  2llnm3N  30051  2llnm4  30052  2llnmeqat  30053  lvolnle3at  30064  4atlem0ae  30076  4atlem0be  30077  4atlem3b  30080  4atlem9  30085  4atlem10a  30086  4atlem10  30088  4atlem11a  30089  4atlem12a  30092  4at2  30096  2lplnm2N  30103  lneq2at  30260  2llnma1b  30268  2llnma1  30269  2llnma3r  30270  2llnma2  30271  2llnma2rN  30272  cdlema1N  30273  paddasslem2  30303  paddasslem16  30317  pmodlem1  30328  pmod2iN  30331  hlmod1i  30338  atmod2i1  30343  atmod2i2  30344  atmod3i1  30346  atmod3i2  30347  atmod4i1  30348  atmod4i2  30349  llnexchb2lem  30350  llnexch2N  30352  dalawlem3  30355  dalawlem4  30356  dalawlem5  30357  dalawlem6  30358  dalawlem7  30359  dalawlem8  30360  dalawlem9  30361  dalawlem11  30363  dalawlem12  30364  dalawlem13  30365  dalawlem15  30367  osumcllem7N  30444  osumcllem9N  30446  pl42lem1N  30461  4atexlemswapqr  30545  4atex2  30559  4atex2-0bOLDN  30561  trlval4  30670  cdlemc5  30677  cdlemc6  30678  cdlemd2  30681  cdlemd4  30683  cdlemd6  30685  cdleme00a  30691  cdleme0e  30699  cdleme4  30720  cdleme4a  30721  cdleme5  30722  cdleme9  30735  cdleme16aN  30741  cdleme11c  30743  cdleme11dN  30744  cdleme11e  30745  cdleme11g  30747  cdleme11h  30748  cdleme11j  30749  cdleme11k  30750  cdleme11l  30751  cdleme11  30752  cdleme12  30753  cdleme13  30754  cdleme14  30755  cdleme15a  30756  cdleme15c  30758  cdleme16b  30761  cdleme16c  30762  cdleme16d  30763  cdleme16e  30764  cdleme16f  30765  cdleme17d1  30771  cdleme0nex  30772  cdleme18a  30773  cdleme18b  30774  cdleme18c  30775  cdleme18d  30777  cdlemednpq  30781  cdlemednuN  30782  cdleme20zN  30783  cdleme20y  30784  cdleme19a  30785  cdleme19b  30786  cdleme19d  30788  cdleme19e  30789  cdleme20aN  30791  cdleme20d  30794  cdleme20f  30796  cdleme20g  30797  cdleme20i  30799  cdleme20j  30800  cdleme20l1  30802  cdleme20l2  30803  cdleme20l  30804  cdleme20m  30805  cdleme21b  30808  cdleme21c  30809  cdleme21e  30813  cdleme21j  30818  cdleme22aa  30821  cdleme22a  30822  cdleme22b  30823  cdleme22cN  30824  cdleme22d  30825  cdleme22e  30826  cdleme22eALTN  30827  cdleme22f  30828  cdleme26fALTN  30844  cdleme26f  30845  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme27N  30851  cdleme28a  30852  cdleme28b  30853  cdleme30a  30860  cdlemefs31fv1  30906  cdleme32b  30924  cdleme32c  30925  cdleme32e  30927  cdleme35h  30938  cdleme36a  30942  cdleme36m  30943  cdleme41sn3aw  30956  cdleme41sn4aw  30957  cdleme41fva11  30959  cdleme42k  30966  cdleme43cN  30973  cdleme46f2g1  30976  cdlemeg46fjgN  31003  cdlemeg46fjv  31005  cdlemeg46frv  31007  cdlemeg46rgv  31010  cdlemeg46req  31011  cdlemeg46gfv  31012  cdleme50trn2a  31032  cdlemg4a  31090  cdlemg4d  31095  cdlemg4e  31096  cdlemg4f  31097  cdlemg8c  31111  cdlemg9a  31114  cdlemg9b  31115  cdlemg10a  31122  cdlemg10  31123  cdlemg12b  31126  cdlemg12f  31130  cdlemg12g  31131  cdlemg12  31132  cdlemg17dN  31145  cdlemg17dALTN  31146  cdlemg17e  31147  cdlemg17f  31148  cdlemg17g  31149  cdlemg17i  31151  cdlemg17ir  31152  cdlemg17pq  31154  cdlemg17bq  31155  cdlemg17iqN  31156  cdlemg17  31159  cdlemg18b  31161  cdlemg18c  31162  cdlemg18d  31163  cdlemg18  31164  cdlemg19  31166  cdlemg21  31168  cdlemg28a  31175  cdlemg31b0a  31177  cdlemg27b  31178  cdlemg33b0  31183  cdlemg28b  31185  cdlemg28  31186  cdlemg35  31195  cdlemg36  31196  cdlemg44a  31213  cdlemh  31299  cdlemi2  31301  cdlemj1  31303  tendocan  31306  cdlemk5a  31317  cdlemk5  31318  cdlemki  31323  cdlemkvcl  31324  cdlemk10  31325  cdlemksv2  31329  cdlemk7  31330  cdlemk11  31331  cdlemk12  31332  cdlemkoatnle  31333  cdlemk15  31337  cdlemk16a  31338  cdlemk16  31339  cdlemk1u  31341  cdlemk5u  31343  cdlemk6u  31344  cdlemk18  31350  cdlemk19  31351  cdlemk7u  31352  cdlemk11u  31353  cdlemk12u  31354  cdlemk21N  31355  cdlemk20  31356  cdlemkoatnle-2N  31357  cdlemk13-2N  31358  cdlemkole-2N  31359  cdlemk14-2N  31360  cdlemk15-2N  31361  cdlemk16-2N  31362  cdlemk17-2N  31363  cdlemk18-2N  31368  cdlemk19-2N  31369  cdlemk22  31375  cdlemk30  31376  cdlemkuel-3  31380  cdlemkuv2-3N  31381  cdlemk18-3N  31382  cdlemkfid1N  31403  cdlemkid1  31404  cdlemkfid3N  31407  cdlemky  31408  cdlemk11ta  31411  cdlemk47  31431  cdlemk48  31432  cdlemk49  31433  cdlemk50  31434  cdlemk51  31435  cdlemk52  31436  cdlemk53a  31437  cdlemk53  31439  cdlemk54  31440  cdlemk55a  31441  cdlemkyyN  31444  cdlemk43N  31445  cdlemk55u1  31447  cdlemk55u  31448  cdlemk39u1  31449  cdlemk19u1  31451  cdleml1N  31458  cdleml2N  31459  cdleml3N  31460  dia2dimlem6  31552  cdlemn2  31678  cdlemn2a  31679  cdlemn5pre  31683  cdlemn11a  31690  dihjustlem  31699  dihjust  31700  dihmeetlem15N  31804  lclkrlem2y  32014
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