Theorem simp31 1032

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

Assertion

Ref	Expression
simp31

Proof of Theorem simp31

Step	Hyp	Ref	Expression
1		simp1 996	. 2
2	1	3ad2ant3 1019	1

Syntax hints:  ->wi 4  /\w3a 973

This theorem is referenced by:  simpl31  1077  simpr31  1086  simp131  1131  simp231  1140  simp331  1149  smogt  7057  frlmphl  18812  mdetuni0  19123  mdetmul  19125  gsummatr01lem3  19159  decpmatmullem  19272  tsmsxp  20657  log2sumbnd  23729  ax5seg  24241  iocinioc2  27590  totprob  28366  cgrtr  29642  cgrtr3  29644  ofscom  29657  cgrextend  29658  segconeq  29660  ifscgr  29694  btwnxfr  29706  colinearxfr  29725  brofs2  29727  brifs2  29728  fscgr  29730  btwnconn1lem1  29737  btwnconn1lem2  29738  btwnconn1lem5  29741  btwnconn1lem6  29742  btwnconn1lem7  29743  btwnconn1lem8  29744  btwnconn1lem9  29745  btwnconn1lem10  29746  btwnconn1lem11  29747  btwnconn1lem12  29748  seglecgr12im  29760  seglecgr12  29761  segletr  29764  outsideofeq  29780  ivthALT  30153  fmuldfeq  31577  lshpkrlem5  34839  lshpkrlem6  34840  exatleN  35128  atbtwn  35170  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  2atmat  35285  4atlem11b  35332  4atlem11  35333  4at  35337  4at2  35338  2lplnja  35343  2lplnj  35344  dalemswapyz  35380  dalemccnedd  35411  cdlemb  35518  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  4atex2  35801  4atex2-0bOLDN  35803  4atex3  35805  ltrn11at  35871  trlval3  35912  cdlemd3  35925  cdleme0moN  35950  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  cdleme15b  36000  cdleme15c  36001  cdleme16b  36004  cdleme16c  36005  cdleme16d  36006  cdleme16e  36007  cdleme16f  36008  cdleme17c  36013  cdleme18c  36018  cdleme18d  36020  cdlemeda  36023  cdleme19a  36029  cdleme19b  36030  cdleme19c  36031  cdleme20aN  36035  cdleme20bN  36036  cdleme20d  36038  cdleme20i  36043  cdleme20j  36044  cdleme20l1  36046  cdleme20l2  36047  cdleme21d  36056  cdleme21e  36057  cdleme21f  36058  cdleme22aa  36065  cdleme22e  36070  cdleme22eALTN  36071  cdleme22f2  36073  cdleme22g  36074  cdleme23b  36076  cdleme26eALTN  36087  cdleme26fALTN  36088  cdleme26f  36089  cdleme26f2ALTN  36090  cdleme26f2  36091  cdleme28a  36096  cdleme28b  36097  cdleme32b  36168  cdleme32c  36169  cdleme32e  36171  cdleme35h  36182  cdleme35sn2aw  36184  cdleme41sn3aw  36200  cdleme41sn4aw  36201  cdlemeg46gfre  36258  cdlemf1  36287  cdlemg1cex  36314  cdlemg2ce  36318  cdlemg4d  36339  cdlemg4e  36340  cdlemg4f  36341  cdlemg4  36343  cdlemg6d  36347  cdlemg6e  36348  cdlemg7fvN  36350  cdlemg8b  36354  cdlemg8c  36355  cdlemg9a  36358  cdlemg9b  36359  cdlemg9  36360  cdlemg11aq  36364  cdlemg10a  36366  cdlemg12a  36369  cdlemg12b  36370  cdlemg12c  36371  cdlemg12d  36372  cdlemg13  36378  cdlemg14f  36379  cdlemg14g  36380  cdlemg17b  36388  cdlemg17dN  36389  cdlemg17e  36391  cdlemg17i  36395  cdlemg17pq  36398  cdlemg17iqN  36400  cdlemg18c  36406  cdlemg18d  36407  cdlemg18  36408  cdlemg19  36410  cdlemg21  36412  cdlemg27a  36418  cdlemg31b0N  36420  cdlemg27b  36422  cdlemg31c  36425  cdlemg33b0  36427  cdlemg33c0  36428  cdlemg33  36437  cdlemg35  36439  cdlemg43  36456  cdlemg44a  36457  cdlemg46  36461  cdlemh2  36542  cdlemh  36543  cdlemj1  36547  cdlemk3  36559  cdlemk5  36562  cdlemk6  36563  cdlemki  36567  cdlemksv2  36573  cdlemk12  36576  cdlemk15  36581  cdlemk16  36583  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  cdlemk20-2N  36618  cdlemk22  36619  cdlemk30  36620  cdlemk31  36622  cdlemk24-3  36629  cdlemkid2  36650  cdlemkfid3N  36651  cdlemk11ta  36655  cdlemkid3N  36659  cdlemk11tc  36671  cdlemk45  36673  cdlemk46  36674  cdlemk47  36675  cdlemk52  36680  cdlemk53a  36681  cdlemk53b  36682  cdleml1N  36702  cdleml3N  36704  cdlemn7  36930  cdlemn10  36933  dihordlem7  36941  dihord1  36945  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