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

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

Proof of Theorem simp33
StepHypRef Expression
1 simp3 998 . 2
213ad2ant3 1019 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  simpl33  1079  simpr33  1088  simp133  1133  simp233  1142  simp333  1151  smogt  7057  bitsfzo  14085  frlmphl  18812  mdetunilem4  19117  mdetuni0  19123  mdetmul  19125  decpmatmullem  19272  logexprlim  23500  ax5seg  24241  iocinioc2  27590  cgrtr  29642  cgrtr3  29644  ofscom  29657  segconeq  29660  btwnxfr  29706  colinearxfr  29725  fscgr  29730  btwnconn1lem1  29737  btwnconn1lem2  29738  btwnconn1lem5  29741  btwnconn1lem6  29742  btwnconn1lem8  29744  btwnconn1lem9  29745  btwnconn1lem10  29746  btwnconn1lem11  29747  btwnconn1lem12  29748  brsegle2  29759  seglecgr12im  29760  seglecgr12  29761  segletr  29764  outsideofeq  29780  fmuldfeq  31577  bnj966  34002  lshpkrlem5  34839  lshpkrlem6  34840  atbtwnexOLDN  35171  atbtwnex  35172  4noncolr3  35177  3dimlem3a  35184  3dimlem4a  35187  3dim1  35191  3dim2  35192  1cvrat  35200  2atjlej  35203  hlatexch4  35205  ps-2b  35206  2atm  35251  ps-2c  35252  lvolex3N  35262  2atmat  35285  lvolnlelpln  35309  4atlem10  35330  4atlem11b  35332  4atlem11  35333  4at  35337  4at2  35338  2lplnja  35343  2lplnj  35344  dalemclccjdd  35412  paddasslem5  35548  paddasslem15  35558  pmodlem1  35570  dalawlem1  35595  dalawlem3  35597  dalawlem4  35598  dalawlem5  35599  dalawlem6  35600  dalawlem7  35601  dalawlem8  35602  dalawlem9  35603  dalawlem11  35605  dalawlem12  35606  dalawlem15  35609  osumcllem5N  35684  osumcllem6N  35685  lhpexle3lem  35735  lhpmcvr4N  35750  lhpmcvr6N  35752  4atexlemex6  35798  4atex2  35801  4atex2-0bOLDN  35803  4atex3  35805  ltrn11at  35871  cdlemd3  35925  cdleme7aa  35967  cdleme7b  35969  cdleme7c  35970  cdleme7d  35971  cdleme7ga  35973  cdleme16aN  35984  cdleme11dN  35987  cdleme11e  35988  cdleme11l  35994  cdleme11  35995  cdleme12  35996  cdleme14  35998  cdleme15c  36001  cdleme16b  36004  cdleme16d  36006  cdleme17b  36012  cdleme17c  36013  cdleme18c  36018  cdleme18d  36020  cdlemeda  36023  cdlemednpq  36024  cdleme19a  36029  cdleme19c  36031  cdleme20aN  36035  cdleme20bN  36036  cdleme20d  36038  cdleme20f  36040  cdleme20g  36041  cdleme20j  36044  cdleme20l1  36046  cdleme21f  36058  cdleme22aa  36065  cdleme22a  36066  cdleme22cN  36068  cdleme22e  36070  cdleme22f2  36073  cdleme22g  36074  cdleme23b  36076  cdleme23c  36077  cdleme26e  36085  cdleme26fALTN  36088  cdleme26f  36089  cdleme26f2ALTN  36090  cdleme26f2  36091  cdleme28a  36096  cdleme28b  36097  cdleme32b  36168  cdleme32c  36169  cdleme32e  36171  cdleme35h2  36183  cdleme38m  36189  cdleme41sn4aw  36201  cdlemf1  36287  cdlemg1cex  36314  cdlemg2ce  36318  cdlemg4d  36339  cdlemg4f  36341  cdlemg7fvN  36350  cdlemg8a  36353  cdlemg8b  36354  cdlemg8c  36355  cdlemg9a  36358  cdlemg11a  36363  cdlemg11aq  36364  cdlemg10a  36366  cdlemg11b  36368  cdlemg12a  36369  cdlemg12b  36370  cdlemg12d  36372  cdlemg12e  36373  cdlemg12f  36374  cdlemg12g  36375  cdlemg12  36376  cdlemg13a  36377  cdlemg13  36378  cdlemg14f  36379  cdlemg14g  36380  cdlemg17b  36388  cdlemg17dN  36389  cdlemg17e  36391  cdlemg17h  36394  cdlemg17pq  36398  cdlemg17iqN  36400  cdlemg18b  36405  cdlemg18c  36406  cdlemg18d  36407  cdlemg18  36408  cdlemg19  36410  cdlemg21  36412  cdlemg27a  36418  cdlemg31b0N  36420  cdlemg27b  36422  cdlemg33b0  36427  cdlemg33c0  36428  cdlemg28  36430  cdlemg33a  36432  cdlemg35  36439  cdlemg42  36455  cdlemg44a  36457  cdlemg47  36462  cdlemh2  36542  cdlemh  36543  cdlemj1  36547  cdlemk3  36559  cdlemk5  36562  cdlemki  36567  cdlemksv2  36573  cdlemk7  36574  cdlemk11  36575  cdlemk12  36576  cdlemkole  36579  cdlemk14  36580  cdlemk15  36581  cdlemk16a  36582  cdlemk16  36583  cdlemkj  36589  cdlemkuv2  36593  cdlemk18  36594  cdlemk19  36595  cdlemk7u  36596  cdlemk12u  36598  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  cdlemk7u-2N  36614  cdlemk11u-2N  36615  cdlemk12u-2N  36616  cdlemk21-2N  36617  cdlemk20-2N  36618  cdlemk22  36619  cdlemk30  36620  cdlemk31  36622  cdlemk32  36623  cdlemk24-3  36629  cdlemkid2  36650  cdlemkfid3N  36651  cdlemk45  36673  cdlemk46  36674  cdlemk47  36675  cdlemk52  36680  cdlemk53a  36681  cdleml1N  36702  cdleml3N  36704  cdlemn7  36930  cdlemn10  36933  dihordlem7  36941  dihord1  36945  dihord2a  36946  dihord10  36950  dihord11c  36951  dihord2pre2  36953  hlhilphllem  37689
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