Theorem simp32 1067

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

Syntax hints:   -> wi 4   /\ w3a 1007

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 190  df-an 378  df-3an 1009

This theorem is referenced by:  simpl32  1112  simpr32  1121  simp132  1166  simp232  1175  simp332  1184  smogt  7104  axdc3lem4  8901  bitsfzo  14488  frlmphl  19416  mdetunilem4  19717  mdetuni0  19723  mdetmul  19725  decpmatmullem  19872  logfacbnd3  24230  logexprlim  24232  log2sumbnd  24461  ax5seg  25047  iocinioc2  28436  totprob  29333  cgrtr  30830  cgrtr3  30832  ofscom  30845  cgrextend  30846  segconeq  30848  ifscgr  30882  colinearxfr  30913  brofs2  30915  brifs2  30916  fscgr  30918  btwnconn1lem2  30926  btwnconn1lem9  30933  btwnconn1lem10  30934  btwnconn1lem11  30935  btwnconn1lem12  30936  brsegle2  30947  seglecgr12im  30948  seglecgr12  30949  segletr  30952  outsideofeq  30968  ivthALT  31062  lshpkrlem5  32751  lshpkrlem6  32752  atbtwnexOLDN  33083  atbtwnex  33084  4noncolr3  33089  3dimlem3a  33096  3dim1  33103  3dim2  33104  1cvrat  33112  2atjlej  33115  hlatexch4  33117  ps-2b  33118  2atm  33163  ps-2c  33164  2atmat  33197  4atlem10  33242  4atlem11b  33244  4atlem11  33245  4at  33249  4at2  33250  2lplnja  33255  2lplnj  33256  dalemswapyz  33292  dalem-ddly  33322  cdlemb  33430  paddasslem5  33460  pmodlem1  33482  dalawlem1  33507  dalawlem3  33509  dalawlem4  33510  dalawlem5  33511  dalawlem6  33512  dalawlem7  33513  dalawlem8  33514  dalawlem9  33515  dalawlem11  33517  dalawlem12  33518  dalawlem15  33521  osumcllem5N  33596  osumcllem6N  33597  lhpexle3lem  33647  lhpmcvr4N  33662  lhpmcvr6N  33664  4atexlemex6  33710  4atex2  33713  4atex2-0bOLDN  33715  4atex2-0cOLDN  33716  ltrn11at  33783  trlval3  33824  cdlemd3  33837  cdleme7aa  33879  cdleme7b  33881  cdleme7c  33882  cdleme7d  33883  cdleme7e  33884  cdleme7ga  33885  cdleme7  33886  cdleme16aN  33896  cdleme11dN  33899  cdleme11e  33900  cdleme11l  33906  cdleme11  33907  cdleme12  33908  cdleme14  33910  cdleme15a  33911  cdleme15c  33913  cdleme16c  33917  cdleme16d  33918  cdleme16e  33919  cdleme16f  33920  cdleme17c  33925  cdleme18c  33930  cdlemeda  33935  cdlemednpq  33936  cdleme19a  33941  cdleme19c  33943  cdleme20aN  33947  cdleme20bN  33948  cdleme20l1  33958  cdleme20l2  33959  cdleme22aa  33977  cdleme22a  33978  cdleme22g  33986  cdleme23b  33988  cdleme23c  33989  cdleme26fALTN  34000  cdleme26f  34001  cdleme26f2ALTN  34002  cdleme26f2  34003  cdleme28b  34009  cdleme32b  34080  cdleme32c  34081  cdleme32e  34083  cdleme35h  34094  cdleme35sn2aw  34096  cdleme38m  34101  cdleme40n  34106  cdleme41sn3aw  34112  cdleme41sn4aw  34113  cdlemeg46gfre  34170  cdlemf1  34199  cdlemg1cex  34226  cdlemg2ce  34230  cdlemg4d  34251  cdlemg4  34255  cdlemg7fvN  34262  cdlemg8b  34266  cdlemg8c  34267  cdlemg9a  34270  cdlemg11aq  34276  cdlemg10a  34278  cdlemg12a  34281  cdlemg12b  34282  cdlemg12d  34284  cdlemg12g  34287  cdlemg12  34288  cdlemg13a  34289  cdlemg13  34290  cdlemg14f  34291  cdlemg14g  34292  cdlemg17b  34300  cdlemg17dN  34301  cdlemg17e  34303  cdlemg17pq  34310  cdlemg17iqN  34312  cdlemg18c  34318  cdlemg18d  34319  cdlemg19a  34321  cdlemg19  34322  cdlemg21  34324  cdlemg27a  34330  cdlemg28a  34331  cdlemg31b0N  34332  cdlemg27b  34334  cdlemg31c  34337  cdlemg33b0  34339  cdlemg28  34342  cdlemg33a  34344  cdlemg33  34349  cdlemg35  34351  cdlemg36  34352  cdlemg44a  34369  cdlemg46  34373  cdlemh2  34454  cdlemh  34455  cdlemj1  34459  cdlemk5  34474  cdlemk6  34475  cdlemki  34479  cdlemksv2  34485  cdlemk7  34486  cdlemk11  34487  cdlemkole  34491  cdlemk14  34492  cdlemk16  34495  cdlemk1u  34497  cdlemk18  34506  cdlemk19  34507  cdlemk7u  34508  cdlemk11u  34509  cdlemk33N  34547  cdlemkid2  34562  cdlemkfid3N  34563  cdlemk11ta  34567  cdlemk11tc  34583  cdlemk45  34585  cdlemk46  34586  cdlemk47  34587  cdlemk52  34592  cdlemk53a  34593  cdlemk54  34596  cdlemk55a  34597  cdleml1N  34614  cdleml3N  34616  cdlemn7  34842  cdlemn8  34843  cdlemn10  34845  dihordlem7  34853  dihordlem7b  34854  dihord1  34857  dihord10  34862  dihord11c  34863  dihord2  34866  hlhilphllem  35601  fmuldfeq  37758