Theorem simp32 1043

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

Assertion

Ref	Expression
simp32	|- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> th )

Proof of Theorem simp32

Step	Hyp	Ref	Expression
1		simp2 1007	. 2 |- ( ( ch /\ th /\ ta ) -> th )
2	1	3ad2ant3 1029	1 |- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ w3a 983

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 189  df-an 373  df-3an 985

This theorem is referenced by:  simpl32  1088  simpr32  1097  simp132  1142  simp232  1151  simp332  1160  smogt  7096  axdc3lem4  8889  bitsfzo  14406  frlmphl  19335  mdetunilem4  19636  mdetuni0  19642  mdetmul  19644  decpmatmullem  19791  logfacbnd3  24147  logexprlim  24149  log2sumbnd  24378  ax5seg  24964  iocinioc2  28365  totprob  29266  cgrtr  30762  cgrtr3  30764  ofscom  30777  cgrextend  30778  segconeq  30780  ifscgr  30814  colinearxfr  30845  brofs2  30847  brifs2  30848  fscgr  30850  btwnconn1lem2  30858  btwnconn1lem9  30865  btwnconn1lem10  30866  btwnconn1lem11  30867  btwnconn1lem12  30868  brsegle2  30879  seglecgr12im  30880  seglecgr12  30881  segletr  30884  outsideofeq  30900  ivthALT  30994  lshpkrlem5  32647  lshpkrlem6  32648  atbtwnexOLDN  32979  atbtwnex  32980  4noncolr3  32985  3dimlem3a  32992  3dim1  32999  3dim2  33000  1cvrat  33008  2atjlej  33011  hlatexch4  33013  ps-2b  33014  2atm  33059  ps-2c  33060  2atmat  33093  4atlem10  33138  4atlem11b  33140  4atlem11  33141  4at  33145  4at2  33146  2lplnja  33151  2lplnj  33152  dalemswapyz  33188  dalem-ddly  33218  cdlemb  33326  paddasslem5  33356  pmodlem1  33378  dalawlem1  33403  dalawlem3  33405  dalawlem4  33406  dalawlem5  33407  dalawlem6  33408  dalawlem7  33409  dalawlem8  33410  dalawlem9  33411  dalawlem11  33413  dalawlem12  33414  dalawlem15  33417  osumcllem5N  33492  osumcllem6N  33493  lhpexle3lem  33543  lhpmcvr4N  33558  lhpmcvr6N  33560  4atexlemex6  33606  4atex2  33609  4atex2-0bOLDN  33611  4atex2-0cOLDN  33612  ltrn11at  33679  trlval3  33720  cdlemd3  33733  cdleme7aa  33775  cdleme7b  33777  cdleme7c  33778  cdleme7d  33779  cdleme7e  33780  cdleme7ga  33781  cdleme7  33782  cdleme16aN  33792  cdleme11dN  33795  cdleme11e  33796  cdleme11l  33802  cdleme11  33803  cdleme12  33804  cdleme14  33806  cdleme15a  33807  cdleme15c  33809  cdleme16c  33813  cdleme16d  33814  cdleme16e  33815  cdleme16f  33816  cdleme17c  33821  cdleme18c  33826  cdlemeda  33831  cdlemednpq  33832  cdleme19a  33837  cdleme19c  33839  cdleme20aN  33843  cdleme20bN  33844  cdleme20l1  33854  cdleme20l2  33855  cdleme22aa  33873  cdleme22a  33874  cdleme22g  33882  cdleme23b  33884  cdleme23c  33885  cdleme26fALTN  33896  cdleme26f  33897  cdleme26f2ALTN  33898  cdleme26f2  33899  cdleme28b  33905  cdleme32b  33976  cdleme32c  33977  cdleme32e  33979  cdleme35h  33990  cdleme35sn2aw  33992  cdleme38m  33997  cdleme40n  34002  cdleme41sn3aw  34008  cdleme41sn4aw  34009  cdlemeg46gfre  34066  cdlemf1  34095  cdlemg1cex  34122  cdlemg2ce  34126  cdlemg4d  34147  cdlemg4  34151  cdlemg7fvN  34158  cdlemg8b  34162  cdlemg8c  34163  cdlemg9a  34166  cdlemg11aq  34172  cdlemg10a  34174  cdlemg12a  34177  cdlemg12b  34178  cdlemg12d  34180  cdlemg12g  34183  cdlemg12  34184  cdlemg13a  34185  cdlemg13  34186  cdlemg14f  34187  cdlemg14g  34188  cdlemg17b  34196  cdlemg17dN  34197  cdlemg17e  34199  cdlemg17pq  34206  cdlemg17iqN  34208  cdlemg18c  34214  cdlemg18d  34215  cdlemg19a  34217  cdlemg19  34218  cdlemg21  34220  cdlemg27a  34226  cdlemg28a  34227  cdlemg31b0N  34228  cdlemg27b  34230  cdlemg31c  34233  cdlemg33b0  34235  cdlemg28  34238  cdlemg33a  34240  cdlemg33  34245  cdlemg35  34247  cdlemg36  34248  cdlemg44a  34265  cdlemg46  34269  cdlemh2  34350  cdlemh  34351  cdlemj1  34355  cdlemk5  34370  cdlemk6  34371  cdlemki  34375  cdlemksv2  34381  cdlemk7  34382  cdlemk11  34383  cdlemkole  34387  cdlemk14  34388  cdlemk16  34391  cdlemk1u  34393  cdlemk18  34402  cdlemk19  34403  cdlemk7u  34404  cdlemk11u  34405  cdlemk33N  34443  cdlemkid2  34458  cdlemkfid3N  34459  cdlemk11ta  34463  cdlemk11tc  34479  cdlemk45  34481  cdlemk46  34482  cdlemk47  34483  cdlemk52  34488  cdlemk53a  34489  cdlemk54  34492  cdlemk55a  34493  cdleml1N  34510  cdleml3N  34512  cdlemn7  34738  cdlemn8  34739  cdlemn10  34741  dihordlem7  34749  dihordlem7b  34750  dihord1  34753  dihord10  34758  dihord11c  34759  dihord2  34762  hlhilphllem  35497  fmuldfeq  37529