Theorem simp33 1208

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp33	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏)

Proof of Theorem simp33

Step	Hyp	Ref	Expression
1		simp3 1135	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜏)
2	1	3ad2ant3 1132	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  simp133  1307  simp233  1316  simp333  1325  eqfunresadj  7371  smogt  8396  bitsfzo  16430  frlmphl  21771  mdetunilem4  22600  mdetuni0  22606  mdetmul  22608  decpmatmullem  22756  logexprlim  27246  noinfres  27744  ax5seg  28864  iocinioc2  32670  bnj966  34757  cgrtr  35776  cgrtr3  35778  ofscom  35791  segconeq  35794  btwnxfr  35840  colinearxfr  35859  fscgr  35864  btwnconn1lem1  35871  btwnconn1lem2  35872  btwnconn1lem5  35875  btwnconn1lem6  35876  btwnconn1lem8  35878  btwnconn1lem9  35879  btwnconn1lem10  35880  btwnconn1lem11  35881  btwnconn1lem12  35882  brsegle2  35893  seglecgr12im  35894  seglecgr12  35895  segletr  35898  outsideofeq  35914  lshpkrlem5  38772  lshpkrlem6  38773  atbtwnexOLDN  39106  atbtwnex  39107  4noncolr3  39112  3dimlem3a  39119  3dimlem4a  39122  3dim1  39126  3dim2  39127  1cvrat  39135  2atjlej  39138  hlatexch4  39140  ps-2b  39141  2atm  39186  ps-2c  39187  lvolex3N  39197  2atmat  39220  lvolnlelpln  39244  4atlem10  39265  4atlem11b  39267  4atlem11  39268  4at  39272  4at2  39273  2lplnja  39278  2lplnj  39279  dalemclccjdd  39347  paddasslem5  39483  paddasslem15  39493  pmodlem1  39505  dalawlem1  39530  dalawlem3  39532  dalawlem4  39533  dalawlem5  39534  dalawlem6  39535  dalawlem7  39536  dalawlem8  39537  dalawlem9  39538  dalawlem11  39540  dalawlem12  39541  dalawlem15  39544  osumcllem5N  39619  osumcllem6N  39620  lhpexle3lem  39670  lhpmcvr4N  39685  lhpmcvr6N  39687  4atexlemex6  39733  4atex2  39736  4atex2-0bOLDN  39738  4atex3  39740  ltrn11at  39806  cdlemd3  39859  cdleme7aa  39901  cdleme7b  39903  cdleme7c  39904  cdleme7d  39905  cdleme7ga  39907  cdleme16aN  39918  cdleme11dN  39921  cdleme11e  39922  cdleme11l  39928  cdleme11  39929  cdleme12  39930  cdleme14  39932  cdleme15c  39935  cdleme16b  39938  cdleme16d  39940  cdleme17b  39946  cdleme17c  39947  cdleme18c  39952  cdleme18d  39954  cdlemeda  39957  cdlemednpq  39958  cdleme19a  39962  cdleme19c  39964  cdleme20aN  39968  cdleme20bN  39969  cdleme20d  39971  cdleme20f  39973  cdleme20g  39974  cdleme20j  39977  cdleme20l1  39979  cdleme21f  39991  cdleme22aa  39998  cdleme22a  39999  cdleme22cN  40001  cdleme22e  40003  cdleme22f2  40006  cdleme22g  40007  cdleme23b  40009  cdleme23c  40010  cdleme26e  40018  cdleme26fALTN  40021  cdleme26f  40022  cdleme26f2ALTN  40023  cdleme26f2  40024  cdleme28a  40029  cdleme28b  40030  cdleme32b  40101  cdleme32c  40102  cdleme32e  40104  cdleme35h2  40116  cdleme38m  40122  cdleme41sn4aw  40134  cdlemf1  40220  cdlemg1cex  40247  cdlemg2ce  40251  cdlemg4d  40272  cdlemg4f  40274  cdlemg7fvN  40283  cdlemg8a  40286  cdlemg8b  40287  cdlemg8c  40288  cdlemg9a  40291  cdlemg11a  40296  cdlemg11aq  40297  cdlemg10a  40299  cdlemg11b  40301  cdlemg12a  40302  cdlemg12b  40303  cdlemg12d  40305  cdlemg12e  40306  cdlemg12f  40307  cdlemg12g  40308  cdlemg12  40309  cdlemg13a  40310  cdlemg13  40311  cdlemg14f  40312  cdlemg14g  40313  cdlemg17b  40321  cdlemg17dN  40322  cdlemg17e  40324  cdlemg17h  40327  cdlemg17pq  40331  cdlemg17iqN  40333  cdlemg18b  40338  cdlemg18c  40339  cdlemg18d  40340  cdlemg18  40341  cdlemg19  40343  cdlemg21  40345  cdlemg27a  40351  cdlemg31b0N  40353  cdlemg27b  40355  cdlemg33b0  40360  cdlemg33c0  40361  cdlemg28  40363  cdlemg33a  40365  cdlemg35  40372  cdlemg42  40388  cdlemg44a  40390  cdlemg47  40395  cdlemh2  40475  cdlemh  40476  cdlemj1  40480  cdlemk3  40492  cdlemk5  40495  cdlemki  40500  cdlemksv2  40506  cdlemk7  40507  cdlemk11  40508  cdlemk12  40509  cdlemkole  40512  cdlemk14  40513  cdlemk15  40514  cdlemk16a  40515  cdlemk16  40516  cdlemkj  40522  cdlemkuv2  40526  cdlemk18  40527  cdlemk19  40528  cdlemk7u  40529  cdlemk12u  40531  cdlemkoatnle-2N  40534  cdlemk13-2N  40535  cdlemkole-2N  40536  cdlemk14-2N  40537  cdlemk15-2N  40538  cdlemk16-2N  40539  cdlemk17-2N  40540  cdlemk18-2N  40545  cdlemk19-2N  40546  cdlemk7u-2N  40547  cdlemk11u-2N  40548  cdlemk12u-2N  40549  cdlemk21-2N  40550  cdlemk20-2N  40551  cdlemk22  40552  cdlemk30  40553  cdlemk31  40555  cdlemk32  40556  cdlemk24-3  40562  cdlemkid2  40583  cdlemkfid3N  40584  cdlemk45  40606  cdlemk46  40607  cdlemk47  40608  cdlemk52  40613  cdlemk53a  40614  cdleml1N  40635  cdleml3N  40637  cdlemn7  40862  cdlemn10  40865  dihordlem7  40873  dihord1  40877  dihord2a  40878  dihord10  40882  dihord11c  40883  dihord2pre2  40885  hlhilphllem  41622  fmuldfeq  45153  seposep  48208  iscnrm3rlem8  48230  iscnrm3llem2  48233