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

Theorem simp22 1030
Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
Assertion
Ref Expression
simp22

Proof of Theorem simp22
StepHypRef Expression
1 simp2 997 . 2
213ad2ant2 1018 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  simpl22  1075  simpr22  1084  simp122  1129  simp222  1138  simp322  1147  elfiun  7910  cofsmo  8670  modexp  12301  funcoppc  15244  funcres  15265  catcisolem  15433  1stfcl  15466  2ndfcl  15467  prfcl  15472  evlfcl  15491  curf1cl  15497  curfcl  15501  hofcl  15528  mulgdirlem  16166  pmtrprfv3  16479  mdetunilem4  19117  mdetuni0  19123  mdetmul  19125  prdsxmetlem  20871  isosctrlem3  23154  isosctr  23155  amgmlem  23319  f1otrg  24174  colinearalg  24213  ax5seglem6  24237  ax5seg  24241  axpasch  24244  axeuclidlem  24265  axeuclid  24266  ogrpsub  27707  ogrpaddlt  27708  ogrpsublt  27712  rhmdvd  27811  mclspps  28944  cgrtr  29642  cgrtr3  29644  ofscom  29657  cgrextend  29658  btwnxfr  29706  colinearxfr  29725  lineext  29726  fscgr  29730  linecgr  29731  btwnconn1lem1  29737  btwnconn1lem2  29738  btwnconn1lem3  29739  btwnconn1lem4  29740  btwnconn1lem5  29741  btwnconn1lem6  29742  btwnconn1lem7  29743  seglecgr12im  29760  seglecgr12  29761  segletr  29764  broutsideof3  29776  outsideofeq  29780  lineunray  29797  linecom  29800  bnj966  34002  eqlkr  34824  lshpkrlem5  34839  omlmod1i2N  34985  cvrnbtwn3  35001  cvrcmp2  35009  cvlexch2  35054  cvlexchb2  35056  cvlatexchb2  35060  cvlatexch1  35061  cvlatexch2  35062  cvlatexch3  35063  cvlsupr7  35073  cvlsupr8  35074  atnlej1  35103  atnlej2  35104  2llnneN  35133  cvratlem  35145  atcvrneN  35154  atlelt  35162  2atjm  35169  3noncolr2  35173  3noncolr1N  35174  hlatcon2  35176  3dimlem2  35183  3dim1  35191  3dim2  35192  1cvrat  35200  ps-1  35201  ps-2  35202  2atjlej  35203  hlatexch3N  35204  ps-2b  35206  3atlem1  35207  3atlem5  35211  3atlem6  35212  2atm  35251  ps-2c  35252  lplni2  35261  lplnri3N  35279  llncvrlpln2  35281  2atmat  35285  2llnm2N  35292  2llnm3N  35293  2llnm4  35294  2llnmeqat  35295  lvolnle3at  35306  4atlem0ae  35318  4atlem0be  35319  4atlem3b  35322  4atlem9  35327  4atlem10a  35328  4atlem10  35330  4atlem11a  35331  4atlem12a  35334  4at2  35338  2lplnm2N  35345  lneq2at  35502  2llnma1b  35510  2llnma1  35511  2llnma3r  35512  2llnma2  35513  2llnma2rN  35514  cdlema1N  35515  paddasslem2  35545  paddasslem16  35559  pmodlem1  35570  pmod2iN  35573  hlmod1i  35580  atmod2i1  35585  atmod2i2  35586  atmod3i1  35588  atmod3i2  35589  atmod4i1  35590  atmod4i2  35591  llnexchb2lem  35592  llnexch2N  35594  dalawlem3  35597  dalawlem4  35598  dalawlem5  35599  dalawlem6  35600  dalawlem7  35601  dalawlem8  35602  dalawlem9  35603  dalawlem11  35605  dalawlem12  35606  dalawlem13  35607  dalawlem15  35609  osumcllem7N  35686  osumcllem9N  35688  pl42lem1N  35703  4atexlemswapqr  35787  4atex2  35801  4atex2-0bOLDN  35803  trlval4  35913  cdlemc5  35920  cdlemc6  35921  cdlemd2  35924  cdlemd4  35926  cdlemd6  35928  cdleme00a  35934  cdleme0e  35942  cdleme4  35963  cdleme4a  35964  cdleme5  35965  cdleme9  35978  cdleme16aN  35984  cdleme11c  35986  cdleme11dN  35987  cdleme11e  35988  cdleme11g  35990  cdleme11h  35991  cdleme11j  35992  cdleme11k  35993  cdleme11l  35994  cdleme11  35995  cdleme12  35996  cdleme13  35997  cdleme14  35998  cdleme15a  35999  cdleme15c  36001  cdleme16b  36004  cdleme16c  36005  cdleme16d  36006  cdleme16e  36007  cdleme16f  36008  cdleme17d1  36014  cdleme0nex  36015  cdleme18a  36016  cdleme18b  36017  cdleme18c  36018  cdleme18d  36020  cdlemednpq  36024  cdlemednuN  36025  cdleme20zN  36026  cdleme20y  36027  cdleme20yOLD  36028  cdleme19a  36029  cdleme19b  36030  cdleme19d  36032  cdleme19e  36033  cdleme20aN  36035  cdleme20d  36038  cdleme20f  36040  cdleme20g  36041  cdleme20i  36043  cdleme20j  36044  cdleme20l1  36046  cdleme20l2  36047  cdleme20l  36048  cdleme20m  36049  cdleme21b  36052  cdleme21c  36053  cdleme21e  36057  cdleme21j  36062  cdleme22aa  36065  cdleme22a  36066  cdleme22b  36067  cdleme22cN  36068  cdleme22d  36069  cdleme22e  36070  cdleme22eALTN  36071  cdleme22f  36072  cdleme26fALTN  36088  cdleme26f  36089  cdleme26f2ALTN  36090  cdleme26f2  36091  cdleme27N  36095  cdleme28a  36096  cdleme28b  36097  cdleme30a  36104  cdlemefs31fv1  36150  cdleme32b  36168  cdleme32c  36169  cdleme32e  36171  cdleme35h  36182  cdleme36a  36186  cdleme36m  36187  cdleme41sn3aw  36200  cdleme41sn4aw  36201  cdleme41fva11  36203  cdleme42k  36210  cdleme43cN  36217  cdleme46f2g1  36220  cdlemeg46fjgN  36247  cdlemeg46fjv  36249  cdlemeg46frv  36251  cdlemeg46rgv  36254  cdlemeg46req  36255  cdlemeg46gfv  36256  cdleme50trn2a  36276  cdlemg4a  36334  cdlemg4d  36339  cdlemg4e  36340  cdlemg4f  36341  cdlemg8c  36355  cdlemg9a  36358  cdlemg9b  36359  cdlemg10a  36366  cdlemg10  36367  cdlemg12b  36370  cdlemg12f  36374  cdlemg12g  36375  cdlemg12  36376  cdlemg17dN  36389  cdlemg17dALTN  36390  cdlemg17e  36391  cdlemg17f  36392  cdlemg17g  36393  cdlemg17i  36395  cdlemg17ir  36396  cdlemg17pq  36398  cdlemg17bq  36399  cdlemg17iqN  36400  cdlemg17  36403  cdlemg18b  36405  cdlemg18c  36406  cdlemg18d  36407  cdlemg18  36408  cdlemg19  36410  cdlemg21  36412  cdlemg28a  36419  cdlemg31b0a  36421  cdlemg27b  36422  cdlemg33b0  36427  cdlemg28b  36429  cdlemg28  36430  cdlemg35  36439  cdlemg36  36440  cdlemg44a  36457  cdlemh  36543  cdlemi2  36545  cdlemj1  36547  tendocan  36550  cdlemk5a  36561  cdlemk5  36562  cdlemki  36567  cdlemkvcl  36568  cdlemk10  36569  cdlemksv2  36573  cdlemk7  36574  cdlemk11  36575  cdlemk12  36576  cdlemkoatnle  36577  cdlemk15  36581  cdlemk16a  36582  cdlemk16  36583  cdlemk1u  36585  cdlemk5u  36587  cdlemk6u  36588  cdlemk18  36594  cdlemk19  36595  cdlemk7u  36596  cdlemk11u  36597  cdlemk12u  36598  cdlemk21N  36599  cdlemk20  36600  cdlemkoatnle-2N  36601  cdlemk13-2N  36602  cdlemkole-2N  36603  cdlemk14-2N  36604  cdlemk15-2N  36605  cdlemk16-2N  36606  cdlemk17-2N  36607  cdlemk18-2N  36612  cdlemk19-2N  36613  cdlemk22  36619  cdlemk30  36620  cdlemkuel-3  36624  cdlemkuv2-3N  36625  cdlemk18-3N  36626  cdlemkfid1N  36647  cdlemkid1  36648  cdlemkfid3N  36651  cdlemky  36652  cdlemk11ta  36655  cdlemk47  36675  cdlemk48  36676  cdlemk49  36677  cdlemk50  36678  cdlemk51  36679  cdlemk52  36680  cdlemk53a  36681  cdlemk53  36683  cdlemk54  36684  cdlemk55a  36685  cdlemkyyN  36688  cdlemk43N  36689  cdlemk55u1  36691  cdlemk55u  36692  cdlemk39u1  36693  cdlemk19u1  36695  cdleml1N  36702  cdleml2N  36703  cdleml3N  36704  dia2dimlem6  36796  cdlemn2  36922  cdlemn2a  36923  cdlemn5pre  36927  cdlemn11a  36934  dihjustlem  36943  dihjust  36944  dihmeetlem15N  37048  lclkrlem2y  37258
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 975
  Copyright terms: Public domain W3C validator