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

Theorem simp22 1031
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 998 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
213ad2ant2 1019 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976
This theorem is referenced by:  simpl22  1076  simpr22  1085  simp122  1130  simp222  1139  simp322  1148  elfiun  7892  cofsmo  8652  modexp  12282  funcoppc  15222  funcres  15243  catcisolem  15411  1stfcl  15444  2ndfcl  15445  prfcl  15450  evlfcl  15469  curf1cl  15475  curfcl  15479  hofcl  15506  mulgdirlem  16144  pmtrprfv3  16457  mdetunilem4  19094  mdetuni0  19100  mdetmul  19102  prdsxmetlem  20848  isosctrlem3  23130  isosctr  23131  amgmlem  23295  f1otrg  24150  colinearalg  24189  ax5seglem6  24213  ax5seg  24217  axpasch  24220  axeuclidlem  24241  axeuclid  24242  ogrpsub  27684  ogrpaddlt  27685  ogrpsublt  27689  rhmdvd  27788  mclspps  28921  cgrtr  29617  cgrtr3  29619  ofscom  29632  cgrextend  29633  btwnxfr  29681  colinearxfr  29700  lineext  29701  fscgr  29705  linecgr  29706  btwnconn1lem1  29712  btwnconn1lem2  29713  btwnconn1lem3  29714  btwnconn1lem4  29715  btwnconn1lem5  29716  btwnconn1lem6  29717  btwnconn1lem7  29718  seglecgr12im  29735  seglecgr12  29736  segletr  29739  broutsideof3  29751  outsideofeq  29755  lineunray  29772  linecom  29775  bnj966  33735  eqlkr  34564  lshpkrlem5  34579  omlmod1i2N  34725  cvrnbtwn3  34741  cvrcmp2  34749  cvlexch2  34794  cvlexchb2  34796  cvlatexchb2  34800  cvlatexch1  34801  cvlatexch2  34802  cvlatexch3  34803  cvlsupr7  34813  cvlsupr8  34814  atnlej1  34843  atnlej2  34844  2llnneN  34873  cvratlem  34885  atcvrneN  34894  atlelt  34902  2atjm  34909  3noncolr2  34913  3noncolr1N  34914  hlatcon2  34916  3dimlem2  34923  3dim1  34931  3dim2  34932  1cvrat  34940  ps-1  34941  ps-2  34942  2atjlej  34943  hlatexch3N  34944  ps-2b  34946  3atlem1  34947  3atlem5  34951  3atlem6  34952  2atm  34991  ps-2c  34992  lplni2  35001  lplnri3N  35019  llncvrlpln2  35021  2atmat  35025  2llnm2N  35032  2llnm3N  35033  2llnm4  35034  2llnmeqat  35035  lvolnle3at  35046  4atlem0ae  35058  4atlem0be  35059  4atlem3b  35062  4atlem9  35067  4atlem10a  35068  4atlem10  35070  4atlem11a  35071  4atlem12a  35074  4at2  35078  2lplnm2N  35085  lneq2at  35242  2llnma1b  35250  2llnma1  35251  2llnma3r  35252  2llnma2  35253  2llnma2rN  35254  cdlema1N  35255  paddasslem2  35285  paddasslem16  35299  pmodlem1  35310  pmod2iN  35313  hlmod1i  35320  atmod2i1  35325  atmod2i2  35326  atmod3i1  35328  atmod3i2  35329  atmod4i1  35330  atmod4i2  35331  llnexchb2lem  35332  llnexch2N  35334  dalawlem3  35337  dalawlem4  35338  dalawlem5  35339  dalawlem6  35340  dalawlem7  35341  dalawlem8  35342  dalawlem9  35343  dalawlem11  35345  dalawlem12  35346  dalawlem13  35347  dalawlem15  35349  osumcllem7N  35426  osumcllem9N  35428  pl42lem1N  35443  4atexlemswapqr  35527  4atex2  35541  4atex2-0bOLDN  35543  trlval4  35653  cdlemc5  35660  cdlemc6  35661  cdlemd2  35664  cdlemd4  35666  cdlemd6  35668  cdleme00a  35674  cdleme0e  35682  cdleme4  35703  cdleme4a  35704  cdleme5  35705  cdleme9  35718  cdleme16aN  35724  cdleme11c  35726  cdleme11dN  35727  cdleme11e  35728  cdleme11g  35730  cdleme11h  35731  cdleme11j  35732  cdleme11k  35733  cdleme11l  35734  cdleme11  35735  cdleme12  35736  cdleme13  35737  cdleme14  35738  cdleme15a  35739  cdleme15c  35741  cdleme16b  35744  cdleme16c  35745  cdleme16d  35746  cdleme16e  35747  cdleme16f  35748  cdleme17d1  35754  cdleme0nex  35755  cdleme18a  35756  cdleme18b  35757  cdleme18c  35758  cdleme18d  35760  cdlemednpq  35764  cdlemednuN  35765  cdleme20zN  35766  cdleme20y  35767  cdleme20yOLD  35768  cdleme19a  35769  cdleme19b  35770  cdleme19d  35772  cdleme19e  35773  cdleme20aN  35775  cdleme20d  35778  cdleme20f  35780  cdleme20g  35781  cdleme20i  35783  cdleme20j  35784  cdleme20l1  35786  cdleme20l2  35787  cdleme20l  35788  cdleme20m  35789  cdleme21b  35792  cdleme21c  35793  cdleme21e  35797  cdleme21j  35802  cdleme22aa  35805  cdleme22a  35806  cdleme22b  35807  cdleme22cN  35808  cdleme22d  35809  cdleme22e  35810  cdleme22eALTN  35811  cdleme22f  35812  cdleme26fALTN  35828  cdleme26f  35829  cdleme26f2ALTN  35830  cdleme26f2  35831  cdleme27N  35835  cdleme28a  35836  cdleme28b  35837  cdleme30a  35844  cdlemefs31fv1  35890  cdleme32b  35908  cdleme32c  35909  cdleme32e  35911  cdleme35h  35922  cdleme36a  35926  cdleme36m  35927  cdleme41sn3aw  35940  cdleme41sn4aw  35941  cdleme41fva11  35943  cdleme42k  35950  cdleme43cN  35957  cdleme46f2g1  35960  cdlemeg46fjgN  35987  cdlemeg46fjv  35989  cdlemeg46frv  35991  cdlemeg46rgv  35994  cdlemeg46req  35995  cdlemeg46gfv  35996  cdleme50trn2a  36016  cdlemg4a  36074  cdlemg4d  36079  cdlemg4e  36080  cdlemg4f  36081  cdlemg8c  36095  cdlemg9a  36098  cdlemg9b  36099  cdlemg10a  36106  cdlemg10  36107  cdlemg12b  36110  cdlemg12f  36114  cdlemg12g  36115  cdlemg12  36116  cdlemg17dN  36129  cdlemg17dALTN  36130  cdlemg17e  36131  cdlemg17f  36132  cdlemg17g  36133  cdlemg17i  36135  cdlemg17ir  36136  cdlemg17pq  36138  cdlemg17bq  36139  cdlemg17iqN  36140  cdlemg17  36143  cdlemg18b  36145  cdlemg18c  36146  cdlemg18d  36147  cdlemg18  36148  cdlemg19  36150  cdlemg21  36152  cdlemg28a  36159  cdlemg31b0a  36161  cdlemg27b  36162  cdlemg33b0  36167  cdlemg28b  36169  cdlemg28  36170  cdlemg35  36179  cdlemg36  36180  cdlemg44a  36197  cdlemh  36283  cdlemi2  36285  cdlemj1  36287  tendocan  36290  cdlemk5a  36301  cdlemk5  36302  cdlemki  36307  cdlemkvcl  36308  cdlemk10  36309  cdlemksv2  36313  cdlemk7  36314  cdlemk11  36315  cdlemk12  36316  cdlemkoatnle  36317  cdlemk15  36321  cdlemk16a  36322  cdlemk16  36323  cdlemk1u  36325  cdlemk5u  36327  cdlemk6u  36328  cdlemk18  36334  cdlemk19  36335  cdlemk7u  36336  cdlemk11u  36337  cdlemk12u  36338  cdlemk21N  36339  cdlemk20  36340  cdlemkoatnle-2N  36341  cdlemk13-2N  36342  cdlemkole-2N  36343  cdlemk14-2N  36344  cdlemk15-2N  36345  cdlemk16-2N  36346  cdlemk17-2N  36347  cdlemk18-2N  36352  cdlemk19-2N  36353  cdlemk22  36359  cdlemk30  36360  cdlemkuel-3  36364  cdlemkuv2-3N  36365  cdlemk18-3N  36366  cdlemkfid1N  36387  cdlemkid1  36388  cdlemkfid3N  36391  cdlemky  36392  cdlemk11ta  36395  cdlemk47  36415  cdlemk48  36416  cdlemk49  36417  cdlemk50  36418  cdlemk51  36419  cdlemk52  36420  cdlemk53a  36421  cdlemk53  36423  cdlemk54  36424  cdlemk55a  36425  cdlemkyyN  36428  cdlemk43N  36429  cdlemk55u1  36431  cdlemk55u  36432  cdlemk39u1  36433  cdlemk19u1  36435  cdleml1N  36442  cdleml2N  36443  cdleml3N  36444  dia2dimlem6  36536  cdlemn2  36662  cdlemn2a  36663  cdlemn5pre  36667  cdlemn11a  36674  dihjustlem  36683  dihjust  36684  dihmeetlem15N  36788  lclkrlem2y  36998
  Copyright terms: Public domain W3C validator