Theorem simp32 1098

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

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpl32  1143  simpr32  1152  simp132  1197  simp232  1206  simp332  1215  smogt  7464  axdc3lem4  9275  bitsfzo  15157  frlmphl  20120  mdetunilem4  20421  mdetuni0  20427  mdetmul  20429  decpmatmullem  20576  logfacbnd3  24948  logexprlim  24950  log2sumbnd  25233  ax5seg  25818  iocinioc2  29541  totprob  30489  eqfunresadj  31659  nosupfv  31852  nosupres  31853  cgrtr  32099  cgrtr3  32101  ofscom  32114  cgrextend  32115  segconeq  32117  ifscgr  32151  colinearxfr  32182  brofs2  32184  brifs2  32185  fscgr  32187  btwnconn1lem2  32195  btwnconn1lem9  32202  btwnconn1lem10  32203  btwnconn1lem11  32204  btwnconn1lem12  32205  brsegle2  32216  seglecgr12im  32217  seglecgr12  32218  segletr  32221  outsideofeq  32237  ivthALT  32330  lshpkrlem5  34401  lshpkrlem6  34402  atbtwnexOLDN  34733  atbtwnex  34734  4noncolr3  34739  3dimlem3a  34746  3dim1  34753  3dim2  34754  1cvrat  34762  2atjlej  34765  hlatexch4  34767  ps-2b  34768  2atm  34813  ps-2c  34814  2atmat  34847  4atlem10  34892  4atlem11b  34894  4atlem11  34895  4at  34899  4at2  34900  2lplnja  34905  2lplnj  34906  dalemswapyz  34942  dalem-ddly  34972  cdlemb  35080  paddasslem5  35110  pmodlem1  35132  dalawlem1  35157  dalawlem3  35159  dalawlem4  35160  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem9  35165  dalawlem11  35167  dalawlem12  35168  dalawlem15  35171  osumcllem5N  35246  osumcllem6N  35247  lhpexle3lem  35297  lhpmcvr4N  35312  lhpmcvr6N  35314  4atexlemex6  35360  4atex2  35363  4atex2-0bOLDN  35365  4atex2-0cOLDN  35366  ltrn11at  35433  trlval3  35474  cdlemd3  35487  cdleme7aa  35529  cdleme7b  35531  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme16aN  35546  cdleme11dN  35549  cdleme11e  35550  cdleme11l  35556  cdleme11  35557  cdleme12  35558  cdleme14  35560  cdleme15a  35561  cdleme15c  35563  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme17c  35575  cdleme18c  35580  cdlemeda  35585  cdlemednpq  35586  cdleme19a  35591  cdleme19c  35593  cdleme20aN  35597  cdleme20bN  35598  cdleme20l1  35608  cdleme20l2  35609  cdleme22aa  35627  cdleme22a  35628  cdleme22g  35636  cdleme23b  35638  cdleme23c  35639  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme28b  35659  cdleme32b  35730  cdleme32c  35731  cdleme32e  35733  cdleme35h  35744  cdleme35sn2aw  35746  cdleme38m  35751  cdleme40n  35756  cdleme41sn3aw  35762  cdleme41sn4aw  35763  cdlemeg46gfre  35820  cdlemf1  35849  cdlemg1cex  35876  cdlemg2ce  35880  cdlemg4d  35901  cdlemg4  35905  cdlemg7fvN  35912  cdlemg8b  35916  cdlemg8c  35917  cdlemg9a  35920  cdlemg11aq  35926  cdlemg10a  35928  cdlemg12a  35931  cdlemg12b  35932  cdlemg12d  35934  cdlemg12g  35937  cdlemg12  35938  cdlemg13a  35939  cdlemg13  35940  cdlemg14f  35941  cdlemg14g  35942  cdlemg17b  35950  cdlemg17dN  35951  cdlemg17e  35953  cdlemg17pq  35960  cdlemg17iqN  35962  cdlemg18c  35968  cdlemg18d  35969  cdlemg19a  35971  cdlemg19  35972  cdlemg21  35974  cdlemg27a  35980  cdlemg28a  35981  cdlemg31b0N  35982  cdlemg27b  35984  cdlemg31c  35987  cdlemg33b0  35989  cdlemg28  35992  cdlemg33a  35994  cdlemg33  35999  cdlemg35  36001  cdlemg36  36002  cdlemg44a  36019  cdlemg46  36023  cdlemh2  36104  cdlemh  36105  cdlemj1  36109  cdlemk5  36124  cdlemk6  36125  cdlemki  36129  cdlemksv2  36135  cdlemk7  36136  cdlemk11  36137  cdlemkole  36141  cdlemk14  36142  cdlemk16  36145  cdlemk1u  36147  cdlemk18  36156  cdlemk19  36157  cdlemk7u  36158  cdlemk11u  36159  cdlemk33N  36197  cdlemkid2  36212  cdlemkfid3N  36213  cdlemk11ta  36217  cdlemk11tc  36233  cdlemk45  36235  cdlemk46  36236  cdlemk47  36237  cdlemk52  36242  cdlemk53a  36243  cdlemk54  36246  cdlemk55a  36247  cdleml1N  36264  cdleml3N  36266  cdlemn7  36492  cdlemn8  36493  cdlemn10  36495  dihordlem7  36503  dihordlem7b  36504  dihord1  36507  dihord10  36512  dihord11c  36513  dihord2  36516  hlhilphllem  37251  fmuldfeq  39815