Theorem simp32 1033

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp32

Proof of Theorem simp32

Step	Hyp	Ref	Expression
1		simp2 997	. 2
2	1	3ad2ant3 1019	1

Syntax hints:  ->wi 4  /\w3a 973

This theorem is referenced by:  simpl32  1078  simpr32  1087  simp132  1132  simp232  1141  simp332  1150  smogt  7057  axdc3lem4  8854  bitsfzo  14085  frlmphl  18812  mdetunilem4  19117  mdetuni0  19123  mdetmul  19125  decpmatmullem  19272  logfacbnd3  23498  logexprlim  23500  log2sumbnd  23729  ax5seg  24241  iocinioc2  27590  totprob  28366  cgrtr  29642  cgrtr3  29644  ofscom  29657  cgrextend  29658  segconeq  29660  ifscgr  29694  colinearxfr  29725  brofs2  29727  brifs2  29728  fscgr  29730  btwnconn1lem2  29738  btwnconn1lem9  29745  btwnconn1lem10  29746  btwnconn1lem11  29747  btwnconn1lem12  29748  brsegle2  29759  seglecgr12im  29760  seglecgr12  29761  segletr  29764  outsideofeq  29780  ivthALT  30153  fmuldfeq  31577  lshpkrlem5  34839  lshpkrlem6  34840  atbtwnexOLDN  35171  atbtwnex  35172  4noncolr3  35177  3dimlem3a  35184  3dim1  35191  3dim2  35192  1cvrat  35200  2atjlej  35203  hlatexch4  35205  ps-2b  35206  2atm  35251  ps-2c  35252  2atmat  35285  4atlem10  35330  4atlem11b  35332  4atlem11  35333  4at  35337  4at2  35338  2lplnja  35343  2lplnj  35344  dalemswapyz  35380  dalem-ddly  35410  cdlemb  35518  paddasslem5  35548  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  4atex2-0cOLDN  35804  ltrn11at  35871  trlval3  35912  cdlemd3  35925  cdleme7aa  35967  cdleme7b  35969  cdleme7c  35970  cdleme7d  35971  cdleme7e  35972  cdleme7ga  35973  cdleme7  35974  cdleme16aN  35984  cdleme11dN  35987  cdleme11e  35988  cdleme11l  35994  cdleme11  35995  cdleme12  35996  cdleme14  35998  cdleme15a  35999  cdleme15c  36001  cdleme16c  36005  cdleme16d  36006  cdleme16e  36007  cdleme16f  36008  cdleme17c  36013  cdleme18c  36018  cdlemeda  36023  cdlemednpq  36024  cdleme19a  36029  cdleme19c  36031  cdleme20aN  36035  cdleme20bN  36036  cdleme20l1  36046  cdleme20l2  36047  cdleme22aa  36065  cdleme22a  36066  cdleme22g  36074  cdleme23b  36076  cdleme23c  36077  cdleme26fALTN  36088  cdleme26f  36089  cdleme26f2ALTN  36090  cdleme26f2  36091  cdleme28b  36097  cdleme32b  36168  cdleme32c  36169  cdleme32e  36171  cdleme35h  36182  cdleme35sn2aw  36184  cdleme38m  36189  cdleme40n  36194  cdleme41sn3aw  36200  cdleme41sn4aw  36201  cdlemeg46gfre  36258  cdlemf1  36287  cdlemg1cex  36314  cdlemg2ce  36318  cdlemg4d  36339  cdlemg4  36343  cdlemg7fvN  36350  cdlemg8b  36354  cdlemg8c  36355  cdlemg9a  36358  cdlemg11aq  36364  cdlemg10a  36366  cdlemg12a  36369  cdlemg12b  36370  cdlemg12d  36372  cdlemg12g  36375  cdlemg12  36376  cdlemg13a  36377  cdlemg13  36378  cdlemg14f  36379  cdlemg14g  36380  cdlemg17b  36388  cdlemg17dN  36389  cdlemg17e  36391  cdlemg17pq  36398  cdlemg17iqN  36400  cdlemg18c  36406  cdlemg18d  36407  cdlemg19a  36409  cdlemg19  36410  cdlemg21  36412  cdlemg27a  36418  cdlemg28a  36419  cdlemg31b0N  36420  cdlemg27b  36422  cdlemg31c  36425  cdlemg33b0  36427  cdlemg28  36430  cdlemg33a  36432  cdlemg33  36437  cdlemg35  36439  cdlemg36  36440  cdlemg44a  36457  cdlemg46  36461  cdlemh2  36542  cdlemh  36543  cdlemj1  36547  cdlemk5  36562  cdlemk6  36563  cdlemki  36567  cdlemksv2  36573  cdlemk7  36574  cdlemk11  36575  cdlemkole  36579  cdlemk14  36580  cdlemk16  36583  cdlemk1u  36585  cdlemk18  36594  cdlemk19  36595  cdlemk7u  36596  cdlemk11u  36597  cdlemk33N  36635  cdlemkid2  36650  cdlemkfid3N  36651  cdlemk11ta  36655  cdlemk11tc  36671  cdlemk45  36673  cdlemk46  36674  cdlemk47  36675  cdlemk52  36680  cdlemk53a  36681  cdlemk54  36684  cdlemk55a  36685  cdleml1N  36702  cdleml3N  36704  cdlemn7  36930  cdlemn8  36931  cdlemn10  36933  dihordlem7  36941  dihordlem7b  36942  dihord1  36945  dihord10  36950  dihord11c  36951  dihord2  36954  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