Theorem simp32 1033

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

Syntax hints:   -> wi 4   /\ w3a 973

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 371  df-3an 975

This theorem is referenced by:  simpl32  1078  simpr32  1087  simp132  1132  simp232  1141  simp332  1150  smogt  7050  axdc3lem4  8845  bitsfzo  13960  frlmphl  18679  mdetunilem4  18984  mdetuni0  18990  mdetmul  18992  decpmatmullem  19139  logfacbnd3  23362  logexprlim  23364  log2sumbnd  23593  ax5seg  24073  iocinioc2  27421  totprob  28198  cgrtr  29576  cgrtr3  29578  ofscom  29591  cgrextend  29592  segconeq  29594  ifscgr  29628  colinearxfr  29659  brofs2  29661  brifs2  29662  fscgr  29664  btwnconn1lem2  29672  btwnconn1lem9  29679  btwnconn1lem10  29680  btwnconn1lem11  29681  btwnconn1lem12  29682  brsegle2  29693  seglecgr12im  29694  seglecgr12  29695  segletr  29698  outsideofeq  29714  ivthALT  30087  fmuldfeq  31462  lshpkrlem5  34317  lshpkrlem6  34318  atbtwnexOLDN  34649  atbtwnex  34650  4noncolr3  34655  3dimlem3a  34662  3dim1  34669  3dim2  34670  1cvrat  34678  2atjlej  34681  hlatexch4  34683  ps-2b  34684  2atm  34729  ps-2c  34730  2atmat  34763  4atlem10  34808  4atlem11b  34810  4atlem11  34811  4at  34815  4at2  34816  2lplnja  34821  2lplnj  34822  dalemswapyz  34858  dalem-ddly  34888  cdlemb  34996  paddasslem5  35026  pmodlem1  35048  dalawlem1  35073  dalawlem3  35075  dalawlem4  35076  dalawlem5  35077  dalawlem6  35078  dalawlem7  35079  dalawlem8  35080  dalawlem9  35081  dalawlem11  35083  dalawlem12  35084  dalawlem15  35087  osumcllem5N  35162  osumcllem6N  35163  lhpexle3lem  35213  lhpmcvr4N  35228  lhpmcvr6N  35230  4atexlemex6  35276  4atex2  35279  4atex2-0bOLDN  35281  4atex2-0cOLDN  35282  ltrn11at  35349  trlval3  35389  cdlemd3  35402  cdleme7aa  35444  cdleme7b  35446  cdleme7c  35447  cdleme7d  35448  cdleme7e  35449  cdleme7ga  35450  cdleme7  35451  cdleme16aN  35461  cdleme11dN  35464  cdleme11e  35465  cdleme11l  35471  cdleme11  35472  cdleme12  35473  cdleme14  35475  cdleme15a  35476  cdleme15c  35478  cdleme16c  35482  cdleme16d  35483  cdleme16e  35484  cdleme16f  35485  cdleme17c  35490  cdleme18c  35495  cdlemeda  35500  cdlemednpq  35501  cdleme19a  35505  cdleme19c  35507  cdleme20aN  35511  cdleme20bN  35512  cdleme20l1  35522  cdleme20l2  35523  cdleme22aa  35541  cdleme22a  35542  cdleme22g  35550  cdleme23b  35552  cdleme23c  35553  cdleme26fALTN  35564  cdleme26f  35565  cdleme26f2ALTN  35566  cdleme26f2  35567  cdleme28b  35573  cdleme32b  35644  cdleme32c  35645  cdleme32e  35647  cdleme35h  35658  cdleme35sn2aw  35660  cdleme38m  35665  cdleme40n  35670  cdleme41sn3aw  35676  cdleme41sn4aw  35677  cdlemeg46gfre  35734  cdlemf1  35763  cdlemg1cex  35790  cdlemg2ce  35794  cdlemg4d  35815  cdlemg4  35819  cdlemg7fvN  35826  cdlemg8b  35830  cdlemg8c  35831  cdlemg9a  35834  cdlemg11aq  35840  cdlemg10a  35842  cdlemg12a  35845  cdlemg12b  35846  cdlemg12d  35848  cdlemg12g  35851  cdlemg12  35852  cdlemg13a  35853  cdlemg13  35854  cdlemg14f  35855  cdlemg14g  35856  cdlemg17b  35864  cdlemg17dN  35865  cdlemg17e  35867  cdlemg17pq  35874  cdlemg17iqN  35876  cdlemg18c  35882  cdlemg18d  35883  cdlemg19a  35885  cdlemg19  35886  cdlemg21  35888  cdlemg27a  35894  cdlemg28a  35895  cdlemg31b0N  35896  cdlemg27b  35898  cdlemg31c  35901  cdlemg33b0  35903  cdlemg28  35906  cdlemg33a  35908  cdlemg33  35913  cdlemg35  35915  cdlemg36  35916  cdlemg44a  35933  cdlemg46  35937  cdlemh2  36018  cdlemh  36019  cdlemj1  36023  cdlemk5  36038  cdlemk6  36039  cdlemki  36043  cdlemksv2  36049  cdlemk7  36050  cdlemk11  36051  cdlemkole  36055  cdlemk14  36056  cdlemk16  36059  cdlemk1u  36061  cdlemk18  36070  cdlemk19  36071  cdlemk7u  36072  cdlemk11u  36073  cdlemk33N  36111  cdlemkid2  36126  cdlemkfid3N  36127  cdlemk11ta  36131  cdlemk11tc  36147  cdlemk45  36149  cdlemk46  36150  cdlemk47  36151  cdlemk52  36156  cdlemk53a  36157  cdlemk54  36160  cdlemk55a  36161  cdleml1N  36178  cdleml3N  36180  cdlemn7  36406  cdlemn8  36407  cdlemn10  36409  dihordlem7  36417  dihordlem7b  36418  dihord1  36421  dihord10  36426  dihord11c  36427  dihord2  36430  hlhilphllem  37165