Theorem simp32 1031

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 995	. 2 |- ( ( ch /\ th /\ ta ) -> th )
2	1	3ad2ant3 1017	1 |- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> th )

Syntax hints:   -> wi 4   /\ w3a 971

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 369  df-3an 973

This theorem is referenced by:  simpl32  1076  simpr32  1085  simp132  1130  simp232  1139  simp332  1148  smogt  6956  axdc3lem4  8746  bitsfzo  14087  frlmphl  18901  mdetunilem4  19202  mdetuni0  19208  mdetmul  19210  decpmatmullem  19357  logfacbnd3  23615  logexprlim  23617  log2sumbnd  23846  ax5seg  24362  iocinioc2  27743  totprob  28549  cgrtr  29795  cgrtr3  29797  ofscom  29810  cgrextend  29811  segconeq  29813  ifscgr  29847  colinearxfr  29878  brofs2  29880  brifs2  29881  fscgr  29883  btwnconn1lem2  29891  btwnconn1lem9  29898  btwnconn1lem10  29899  btwnconn1lem11  29900  btwnconn1lem12  29901  brsegle2  29912  seglecgr12im  29913  seglecgr12  29914  segletr  29917  outsideofeq  29933  ivthALT  30319  fmuldfeq  31743  lshpkrlem5  35252  lshpkrlem6  35253  atbtwnexOLDN  35584  atbtwnex  35585  4noncolr3  35590  3dimlem3a  35597  3dim1  35604  3dim2  35605  1cvrat  35613  2atjlej  35616  hlatexch4  35618  ps-2b  35619  2atm  35664  ps-2c  35665  2atmat  35698  4atlem10  35743  4atlem11b  35745  4atlem11  35746  4at  35750  4at2  35751  2lplnja  35756  2lplnj  35757  dalemswapyz  35793  dalem-ddly  35823  cdlemb  35931  paddasslem5  35961  pmodlem1  35983  dalawlem1  36008  dalawlem3  36010  dalawlem4  36011  dalawlem5  36012  dalawlem6  36013  dalawlem7  36014  dalawlem8  36015  dalawlem9  36016  dalawlem11  36018  dalawlem12  36019  dalawlem15  36022  osumcllem5N  36097  osumcllem6N  36098  lhpexle3lem  36148  lhpmcvr4N  36163  lhpmcvr6N  36165  4atexlemex6  36211  4atex2  36214  4atex2-0bOLDN  36216  4atex2-0cOLDN  36217  ltrn11at  36284  trlval3  36325  cdlemd3  36338  cdleme7aa  36380  cdleme7b  36382  cdleme7c  36383  cdleme7d  36384  cdleme7e  36385  cdleme7ga  36386  cdleme7  36387  cdleme16aN  36397  cdleme11dN  36400  cdleme11e  36401  cdleme11l  36407  cdleme11  36408  cdleme12  36409  cdleme14  36411  cdleme15a  36412  cdleme15c  36414  cdleme16c  36418  cdleme16d  36419  cdleme16e  36420  cdleme16f  36421  cdleme17c  36426  cdleme18c  36431  cdlemeda  36436  cdlemednpq  36437  cdleme19a  36442  cdleme19c  36444  cdleme20aN  36448  cdleme20bN  36449  cdleme20l1  36459  cdleme20l2  36460  cdleme22aa  36478  cdleme22a  36479  cdleme22g  36487  cdleme23b  36489  cdleme23c  36490  cdleme26fALTN  36501  cdleme26f  36502  cdleme26f2ALTN  36503  cdleme26f2  36504  cdleme28b  36510  cdleme32b  36581  cdleme32c  36582  cdleme32e  36584  cdleme35h  36595  cdleme35sn2aw  36597  cdleme38m  36602  cdleme40n  36607  cdleme41sn3aw  36613  cdleme41sn4aw  36614  cdlemeg46gfre  36671  cdlemf1  36700  cdlemg1cex  36727  cdlemg2ce  36731  cdlemg4d  36752  cdlemg4  36756  cdlemg7fvN  36763  cdlemg8b  36767  cdlemg8c  36768  cdlemg9a  36771  cdlemg11aq  36777  cdlemg10a  36779  cdlemg12a  36782  cdlemg12b  36783  cdlemg12d  36785  cdlemg12g  36788  cdlemg12  36789  cdlemg13a  36790  cdlemg13  36791  cdlemg14f  36792  cdlemg14g  36793  cdlemg17b  36801  cdlemg17dN  36802  cdlemg17e  36804  cdlemg17pq  36811  cdlemg17iqN  36813  cdlemg18c  36819  cdlemg18d  36820  cdlemg19a  36822  cdlemg19  36823  cdlemg21  36825  cdlemg27a  36831  cdlemg28a  36832  cdlemg31b0N  36833  cdlemg27b  36835  cdlemg31c  36838  cdlemg33b0  36840  cdlemg28  36843  cdlemg33a  36845  cdlemg33  36850  cdlemg35  36852  cdlemg36  36853  cdlemg44a  36870  cdlemg46  36874  cdlemh2  36955  cdlemh  36956  cdlemj1  36960  cdlemk5  36975  cdlemk6  36976  cdlemki  36980  cdlemksv2  36986  cdlemk7  36987  cdlemk11  36988  cdlemkole  36992  cdlemk14  36993  cdlemk16  36996  cdlemk1u  36998  cdlemk18  37007  cdlemk19  37008  cdlemk7u  37009  cdlemk11u  37010  cdlemk33N  37048  cdlemkid2  37063  cdlemkfid3N  37064  cdlemk11ta  37068  cdlemk11tc  37084  cdlemk45  37086  cdlemk46  37087  cdlemk47  37088  cdlemk52  37093  cdlemk53a  37094  cdlemk54  37097  cdlemk55a  37098  cdleml1N  37115  cdleml3N  37117  cdlemn7  37343  cdlemn8  37344  cdlemn10  37346  dihordlem7  37354  dihordlem7b  37355  dihord1  37358  dihord10  37363  dihord11c  37364  dihord2  37367  hlhilphllem  38102