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

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

Proof of Theorem simp22
StepHypRef Expression
1 simp2 989 . 2
213ad2ant2 1010 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 965
This theorem is referenced by:  simpl22  1067  simpr22  1076  simp122  1121  simp222  1130  simp322  1139  elfiun  7765  cofsmo  8523  modexp  12084  funcoppc  14871  funcres  14892  catcisolem  15060  1stfcl  15093  2ndfcl  15094  prfcl  15099  evlfcl  15118  curf1cl  15124  curfcl  15128  hofcl  15155  mulgdirlem  15737  pmtrprfv3  16046  mdetunilem4  18521  mdetuni0  18527  mdetmul  18529  prdsxmetlem  20043  isosctrlem3  22318  isosctr  22319  amgmlem  22483  f1otrg  23236  colinearalg  23275  ax5seglem6  23299  ax5seg  23303  axpasch  23306  axeuclidlem  23327  axeuclid  23328  ogrpsub  26298  ogrpsublt  26303  rhmdvd  26407  cgrtr  28141  cgrtr3  28143  ofscom  28156  cgrextend  28157  btwnxfr  28205  colinearxfr  28224  lineext  28225  fscgr  28229  linecgr  28230  btwnconn1lem1  28236  btwnconn1lem2  28237  btwnconn1lem3  28238  btwnconn1lem4  28239  btwnconn1lem5  28240  btwnconn1lem6  28241  btwnconn1lem7  28242  seglecgr12im  28259  seglecgr12  28260  segletr  28263  broutsideof3  28275  outsideofeq  28279  lineunray  28296  linecom  28299  bnj966  32218  eqlkr  33025  lshpkrlem5  33040  omlmod1i2N  33186  cvrnbtwn3  33202  cvrcmp2  33210  cvlexch2  33255  cvlexchb2  33257  cvlatexchb2  33261  cvlatexch1  33262  cvlatexch2  33263  cvlatexch3  33264  cvlsupr7  33274  cvlsupr8  33275  atnlej1  33304  atnlej2  33305  2llnneN  33334  cvratlem  33346  atcvrneN  33355  atlelt  33363  2atjm  33370  3noncolr2  33374  3noncolr1N  33375  hlatcon2  33377  3dimlem2  33384  3dim1  33392  3dim2  33393  1cvrat  33401  ps-1  33402  ps-2  33403  2atjlej  33404  hlatexch3N  33405  ps-2b  33407  3atlem1  33408  3atlem5  33412  3atlem6  33413  2atm  33452  ps-2c  33453  lplni2  33462  lplnri3N  33480  llncvrlpln2  33482  2atmat  33486  2llnm2N  33493  2llnm3N  33494  2llnm4  33495  2llnmeqat  33496  lvolnle3at  33507  4atlem0ae  33519  4atlem0be  33520  4atlem3b  33523  4atlem9  33528  4atlem10a  33529  4atlem10  33531  4atlem11a  33532  4atlem12a  33535  4at2  33539  2lplnm2N  33546  lneq2at  33703  2llnma1b  33711  2llnma1  33712  2llnma3r  33713  2llnma2  33714  2llnma2rN  33715  cdlema1N  33716  paddasslem2  33746  paddasslem16  33760  pmodlem1  33771  pmod2iN  33774  hlmod1i  33781  atmod2i1  33786  atmod2i2  33787  atmod3i1  33789  atmod3i2  33790  atmod4i1  33791  atmod4i2  33792  llnexchb2lem  33793  llnexch2N  33795  dalawlem3  33798  dalawlem4  33799  dalawlem5  33800  dalawlem6  33801  dalawlem7  33802  dalawlem8  33803  dalawlem9  33804  dalawlem11  33806  dalawlem12  33807  dalawlem13  33808  dalawlem15  33810  osumcllem7N  33887  osumcllem9N  33889  pl42lem1N  33904  4atexlemswapqr  33988  4atex2  34002  4atex2-0bOLDN  34004  trlval4  34113  cdlemc5  34120  cdlemc6  34121  cdlemd2  34124  cdlemd4  34126  cdlemd6  34128  cdleme00a  34134  cdleme0e  34142  cdleme4  34163  cdleme4a  34164  cdleme5  34165  cdleme9  34178  cdleme16aN  34184  cdleme11c  34186  cdleme11dN  34187  cdleme11e  34188  cdleme11g  34190  cdleme11h  34191  cdleme11j  34192  cdleme11k  34193  cdleme11l  34194  cdleme11  34195  cdleme12  34196  cdleme13  34197  cdleme14  34198  cdleme15a  34199  cdleme15c  34201  cdleme16b  34204  cdleme16c  34205  cdleme16d  34206  cdleme16e  34207  cdleme16f  34208  cdleme17d1  34214  cdleme0nex  34215  cdleme18a  34216  cdleme18b  34217  cdleme18c  34218  cdleme18d  34220  cdlemednpq  34224  cdlemednuN  34225  cdleme20zN  34226  cdleme20y  34227  cdleme19a  34228  cdleme19b  34229  cdleme19d  34231  cdleme19e  34232  cdleme20aN  34234  cdleme20d  34237  cdleme20f  34239  cdleme20g  34240  cdleme20i  34242  cdleme20j  34243  cdleme20l1  34245  cdleme20l2  34246  cdleme20l  34247  cdleme20m  34248  cdleme21b  34251  cdleme21c  34252  cdleme21e  34256  cdleme21j  34261  cdleme22aa  34264  cdleme22a  34265  cdleme22b  34266  cdleme22cN  34267  cdleme22d  34268  cdleme22e  34269  cdleme22eALTN  34270  cdleme22f  34271  cdleme26fALTN  34287  cdleme26f  34288  cdleme26f2ALTN  34289  cdleme26f2  34290  cdleme27N  34294  cdleme28a  34295  cdleme28b  34296  cdleme30a  34303  cdlemefs31fv1  34349  cdleme32b  34367  cdleme32c  34368  cdleme32e  34370  cdleme35h  34381  cdleme36a  34385  cdleme36m  34386  cdleme41sn3aw  34399  cdleme41sn4aw  34400  cdleme41fva11  34402  cdleme42k  34409  cdleme43cN  34416  cdleme46f2g1  34419  cdlemeg46fjgN  34446  cdlemeg46fjv  34448  cdlemeg46frv  34450  cdlemeg46rgv  34453  cdlemeg46req  34454  cdlemeg46gfv  34455  cdleme50trn2a  34475  cdlemg4a  34533  cdlemg4d  34538  cdlemg4e  34539  cdlemg4f  34540  cdlemg8c  34554  cdlemg9a  34557  cdlemg9b  34558  cdlemg10a  34565  cdlemg10  34566  cdlemg12b  34569  cdlemg12f  34573  cdlemg12g  34574  cdlemg12  34575  cdlemg17dN  34588  cdlemg17dALTN  34589  cdlemg17e  34590  cdlemg17f  34591  cdlemg17g  34592  cdlemg17i  34594  cdlemg17ir  34595  cdlemg17pq  34597  cdlemg17bq  34598  cdlemg17iqN  34599  cdlemg17  34602  cdlemg18b  34604  cdlemg18c  34605  cdlemg18d  34606  cdlemg18  34607  cdlemg19  34609  cdlemg21  34611  cdlemg28a  34618  cdlemg31b0a  34620  cdlemg27b  34621  cdlemg33b0  34626  cdlemg28b  34628  cdlemg28  34629  cdlemg35  34638  cdlemg36  34639  cdlemg44a  34656  cdlemh  34742  cdlemi2  34744  cdlemj1  34746  tendocan  34749  cdlemk5a  34760  cdlemk5  34761  cdlemki  34766  cdlemkvcl  34767  cdlemk10  34768  cdlemksv2  34772  cdlemk7  34773  cdlemk11  34774  cdlemk12  34775  cdlemkoatnle  34776  cdlemk15  34780  cdlemk16a  34781  cdlemk16  34782  cdlemk1u  34784  cdlemk5u  34786  cdlemk6u  34787  cdlemk18  34793  cdlemk19  34794  cdlemk7u  34795  cdlemk11u  34796  cdlemk12u  34797  cdlemk21N  34798  cdlemk20  34799  cdlemkoatnle-2N  34800  cdlemk13-2N  34801  cdlemkole-2N  34802  cdlemk14-2N  34803  cdlemk15-2N  34804  cdlemk16-2N  34805  cdlemk17-2N  34806  cdlemk18-2N  34811  cdlemk19-2N  34812  cdlemk22  34818  cdlemk30  34819  cdlemkuel-3  34823  cdlemkuv2-3N  34824  cdlemk18-3N  34825  cdlemkfid1N  34846  cdlemkid1  34847  cdlemkfid3N  34850  cdlemky  34851  cdlemk11ta  34854  cdlemk47  34874  cdlemk48  34875  cdlemk49  34876  cdlemk50  34877  cdlemk51  34878  cdlemk52  34879  cdlemk53a  34880  cdlemk53  34882  cdlemk54  34883  cdlemk55a  34884  cdlemkyyN  34887  cdlemk43N  34888  cdlemk55u1  34890  cdlemk55u  34891  cdlemk39u1  34892  cdlemk19u1  34894  cdleml1N  34901  cdleml2N  34902  cdleml3N  34903  dia2dimlem6  34995  cdlemn2  35121  cdlemn2a  35122  cdlemn5pre  35126  cdlemn11a  35133  dihjustlem  35142  dihjust  35143  dihmeetlem15N  35247  lclkrlem2y  35457
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 967
  Copyright terms: Public domain W3C validator