Theorem simp32 994

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

Syntax hints:   -> wi 4   /\ w3a 936

This theorem is referenced by:  simpl32  1039  simpr32  1048  simp132  1093  simp232  1102  simp332  1111  smogt  6588  axdc3lem4  8289  bitsfzo  12902  logfacbnd3  20960  logexprlim  20962  log2sumbnd  21191  iocinioc2  24095  totprob  24638  ax5seg  25781  cgrtr  25830  cgrtr3  25832  ofscom  25845  cgrextend  25846  segconeq  25848  ifscgr  25882  colinearxfr  25913  brofs2  25915  brifs2  25916  fscgr  25918  btwnconn1lem2  25926  btwnconn1lem9  25933  btwnconn1lem10  25934  btwnconn1lem11  25935  btwnconn1lem12  25936  brsegle2  25947  seglecgr12im  25948  seglecgr12  25949  segletr  25952  outsideofeq  25968  ivthALT  26228  fmuldfeq  27580  lshpkrlem5  29597  lshpkrlem6  29598  atbtwnexOLDN  29929  atbtwnex  29930  4noncolr3  29935  3dimlem3a  29942  3dim1  29949  3dim2  29950  1cvrat  29958  2atjlej  29961  hlatexch4  29963  ps-2b  29964  2atm  30009  ps-2c  30010  2atmat  30043  4atlem10  30088  4atlem11b  30090  4atlem11  30091  4at  30095  4at2  30096  2lplnja  30101  2lplnj  30102  dalemswapyz  30138  dalem-ddly  30168  cdlemb  30276  paddasslem5  30306  pmodlem1  30328  dalawlem1  30353  dalawlem3  30355  dalawlem4  30356  dalawlem5  30357  dalawlem6  30358  dalawlem7  30359  dalawlem8  30360  dalawlem9  30361  dalawlem11  30363  dalawlem12  30364  dalawlem15  30367  osumcllem5N  30442  osumcllem6N  30443  lhpexle3lem  30493  lhpmcvr4N  30508  lhpmcvr6N  30510  4atexlemex6  30556  4atex2  30559  4atex2-0bOLDN  30561  4atex2-0cOLDN  30562  ltrn11at  30629  trlval3  30669  cdlemd3  30682  cdleme7aa  30724  cdleme7b  30726  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme16aN  30741  cdleme11dN  30744  cdleme11e  30745  cdleme11l  30751  cdleme11  30752  cdleme12  30753  cdleme14  30755  cdleme15a  30756  cdleme15c  30758  cdleme16c  30762  cdleme16d  30763  cdleme16e  30764  cdleme16f  30765  cdleme17c  30770  cdleme18c  30775  cdlemeda  30780  cdlemednpq  30781  cdleme19a  30785  cdleme19c  30787  cdleme20aN  30791  cdleme20bN  30792  cdleme20l1  30802  cdleme20l2  30803  cdleme22aa  30821  cdleme22a  30822  cdleme22g  30830  cdleme23b  30832  cdleme23c  30833  cdleme26fALTN  30844  cdleme26f  30845  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme28b  30853  cdleme32b  30924  cdleme32c  30925  cdleme32e  30927  cdleme35h  30938  cdleme35sn2aw  30940  cdleme38m  30945  cdleme40n  30950  cdleme41sn3aw  30956  cdleme41sn4aw  30957  cdlemeg46gfre  31014  cdlemf1  31043  cdlemg1cex  31070  cdlemg2ce  31074  cdlemg4d  31095  cdlemg4  31099  cdlemg7fvN  31106  cdlemg8b  31110  cdlemg8c  31111  cdlemg9a  31114  cdlemg11aq  31120  cdlemg10a  31122  cdlemg12a  31125  cdlemg12b  31126  cdlemg12d  31128  cdlemg12g  31131  cdlemg12  31132  cdlemg13a  31133  cdlemg13  31134  cdlemg14f  31135  cdlemg14g  31136  cdlemg17b  31144  cdlemg17dN  31145  cdlemg17e  31147  cdlemg17pq  31154  cdlemg17iqN  31156  cdlemg18c  31162  cdlemg18d  31163  cdlemg19a  31165  cdlemg19  31166  cdlemg21  31168  cdlemg27a  31174  cdlemg28a  31175  cdlemg31b0N  31176  cdlemg27b  31178  cdlemg31c  31181  cdlemg33b0  31183  cdlemg28  31186  cdlemg33a  31188  cdlemg33  31193  cdlemg35  31195  cdlemg36  31196  cdlemg44a  31213  cdlemg46  31217  cdlemh2  31298  cdlemh  31299  cdlemj1  31303  cdlemk5  31318  cdlemk6  31319  cdlemki  31323  cdlemksv2  31329  cdlemk7  31330  cdlemk11  31331  cdlemkole  31335  cdlemk14  31336  cdlemk16  31339  cdlemk1u  31341  cdlemk18  31350  cdlemk19  31351  cdlemk7u  31352  cdlemk11u  31353  cdlemk33N  31391  cdlemkid2  31406  cdlemkfid3N  31407  cdlemk11ta  31411  cdlemk11tc  31427  cdlemk45  31429  cdlemk46  31430  cdlemk47  31431  cdlemk52  31436  cdlemk53a  31437  cdlemk54  31440  cdlemk55a  31441  cdleml1N  31458  cdleml3N  31460  cdlemn7  31686  cdlemn8  31687  cdlemn10  31689  dihordlem7  31697  dihordlem7b  31698  dihord1  31701  dihord10  31706  dihord11c  31707  dihord2  31710  hlhilphllem  32445

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938