Theorem simp32 1046

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

Syntax hints:   -> wi 4   /\ w3a 986

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 189  df-an 373  df-3an 988

This theorem is referenced by:  simpl32  1091  simpr32  1100  simp132  1145  simp232  1154  simp332  1163  smogt  7091  axdc3lem4  8888  bitsfzo  14421  frlmphl  19351  mdetunilem4  19652  mdetuni0  19658  mdetmul  19660  decpmatmullem  19807  logfacbnd3  24163  logexprlim  24165  log2sumbnd  24394  ax5seg  24980  iocinioc2  28373  totprob  29272  cgrtr  30771  cgrtr3  30773  ofscom  30786  cgrextend  30787  segconeq  30789  ifscgr  30823  colinearxfr  30854  brofs2  30856  brifs2  30857  fscgr  30859  btwnconn1lem2  30867  btwnconn1lem9  30874  btwnconn1lem10  30875  btwnconn1lem11  30876  btwnconn1lem12  30877  brsegle2  30888  seglecgr12im  30889  seglecgr12  30890  segletr  30893  outsideofeq  30909  ivthALT  31003  lshpkrlem5  32692  lshpkrlem6  32693  atbtwnexOLDN  33024  atbtwnex  33025  4noncolr3  33030  3dimlem3a  33037  3dim1  33044  3dim2  33045  1cvrat  33053  2atjlej  33056  hlatexch4  33058  ps-2b  33059  2atm  33104  ps-2c  33105  2atmat  33138  4atlem10  33183  4atlem11b  33185  4atlem11  33186  4at  33190  4at2  33191  2lplnja  33196  2lplnj  33197  dalemswapyz  33233  dalem-ddly  33263  cdlemb  33371  paddasslem5  33401  pmodlem1  33423  dalawlem1  33448  dalawlem3  33450  dalawlem4  33451  dalawlem5  33452  dalawlem6  33453  dalawlem7  33454  dalawlem8  33455  dalawlem9  33456  dalawlem11  33458  dalawlem12  33459  dalawlem15  33462  osumcllem5N  33537  osumcllem6N  33538  lhpexle3lem  33588  lhpmcvr4N  33603  lhpmcvr6N  33605  4atexlemex6  33651  4atex2  33654  4atex2-0bOLDN  33656  4atex2-0cOLDN  33657  ltrn11at  33724  trlval3  33765  cdlemd3  33778  cdleme7aa  33820  cdleme7b  33822  cdleme7c  33823  cdleme7d  33824  cdleme7e  33825  cdleme7ga  33826  cdleme7  33827  cdleme16aN  33837  cdleme11dN  33840  cdleme11e  33841  cdleme11l  33847  cdleme11  33848  cdleme12  33849  cdleme14  33851  cdleme15a  33852  cdleme15c  33854  cdleme16c  33858  cdleme16d  33859  cdleme16e  33860  cdleme16f  33861  cdleme17c  33866  cdleme18c  33871  cdlemeda  33876  cdlemednpq  33877  cdleme19a  33882  cdleme19c  33884  cdleme20aN  33888  cdleme20bN  33889  cdleme20l1  33899  cdleme20l2  33900  cdleme22aa  33918  cdleme22a  33919  cdleme22g  33927  cdleme23b  33929  cdleme23c  33930  cdleme26fALTN  33941  cdleme26f  33942  cdleme26f2ALTN  33943  cdleme26f2  33944  cdleme28b  33950  cdleme32b  34021  cdleme32c  34022  cdleme32e  34024  cdleme35h  34035  cdleme35sn2aw  34037  cdleme38m  34042  cdleme40n  34047  cdleme41sn3aw  34053  cdleme41sn4aw  34054  cdlemeg46gfre  34111  cdlemf1  34140  cdlemg1cex  34167  cdlemg2ce  34171  cdlemg4d  34192  cdlemg4  34196  cdlemg7fvN  34203  cdlemg8b  34207  cdlemg8c  34208  cdlemg9a  34211  cdlemg11aq  34217  cdlemg10a  34219  cdlemg12a  34222  cdlemg12b  34223  cdlemg12d  34225  cdlemg12g  34228  cdlemg12  34229  cdlemg13a  34230  cdlemg13  34231  cdlemg14f  34232  cdlemg14g  34233  cdlemg17b  34241  cdlemg17dN  34242  cdlemg17e  34244  cdlemg17pq  34251  cdlemg17iqN  34253  cdlemg18c  34259  cdlemg18d  34260  cdlemg19a  34262  cdlemg19  34263  cdlemg21  34265  cdlemg27a  34271  cdlemg28a  34272  cdlemg31b0N  34273  cdlemg27b  34275  cdlemg31c  34278  cdlemg33b0  34280  cdlemg28  34283  cdlemg33a  34285  cdlemg33  34290  cdlemg35  34292  cdlemg36  34293  cdlemg44a  34310  cdlemg46  34314  cdlemh2  34395  cdlemh  34396  cdlemj1  34400  cdlemk5  34415  cdlemk6  34416  cdlemki  34420  cdlemksv2  34426  cdlemk7  34427  cdlemk11  34428  cdlemkole  34432  cdlemk14  34433  cdlemk16  34436  cdlemk1u  34438  cdlemk18  34447  cdlemk19  34448  cdlemk7u  34449  cdlemk11u  34450  cdlemk33N  34488  cdlemkid2  34503  cdlemkfid3N  34504  cdlemk11ta  34508  cdlemk11tc  34524  cdlemk45  34526  cdlemk46  34527  cdlemk47  34528  cdlemk52  34533  cdlemk53a  34534  cdlemk54  34537  cdlemk55a  34538  cdleml1N  34555  cdleml3N  34557  cdlemn7  34783  cdlemn8  34784  cdlemn10  34786  dihordlem7  34794  dihordlem7b  34795  dihord1  34798  dihord10  34803  dihord11c  34804  dihord2  34807  hlhilphllem  35542  fmuldfeq  37671