Theorem simp33 1207

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 1134	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜏)
2	1	3ad2ant3 1131	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp133  1306  simp233  1315  simp333  1324  smogt  7998  bitsfzo  15778  frlmphl  20919  mdetunilem4  21218  mdetuni0  21224  mdetmul  21226  decpmatmullem  21373  logexprlim  25795  ax5seg  26718  iocinioc2  30496  bnj966  32211  eqfunresadj  32999  cgrtr  33448  cgrtr3  33450  ofscom  33463  segconeq  33466  btwnxfr  33512  colinearxfr  33531  fscgr  33536  btwnconn1lem1  33543  btwnconn1lem2  33544  btwnconn1lem5  33547  btwnconn1lem6  33548  btwnconn1lem8  33550  btwnconn1lem9  33551  btwnconn1lem10  33552  btwnconn1lem11  33553  btwnconn1lem12  33554  brsegle2  33565  seglecgr12im  33566  seglecgr12  33567  segletr  33570  outsideofeq  33586  lshpkrlem5  36244  lshpkrlem6  36245  atbtwnexOLDN  36577  atbtwnex  36578  4noncolr3  36583  3dimlem3a  36590  3dimlem4a  36593  3dim1  36597  3dim2  36598  1cvrat  36606  2atjlej  36609  hlatexch4  36611  ps-2b  36612  2atm  36657  ps-2c  36658  lvolex3N  36668  2atmat  36691  lvolnlelpln  36715  4atlem10  36736  4atlem11b  36738  4atlem11  36739  4at  36743  4at2  36744  2lplnja  36749  2lplnj  36750  dalemclccjdd  36818  paddasslem5  36954  paddasslem15  36964  pmodlem1  36976  dalawlem1  37001  dalawlem3  37003  dalawlem4  37004  dalawlem5  37005  dalawlem6  37006  dalawlem7  37007  dalawlem8  37008  dalawlem9  37009  dalawlem11  37011  dalawlem12  37012  dalawlem15  37015  osumcllem5N  37090  osumcllem6N  37091  lhpexle3lem  37141  lhpmcvr4N  37156  lhpmcvr6N  37158  4atexlemex6  37204  4atex2  37207  4atex2-0bOLDN  37209  4atex3  37211  ltrn11at  37277  cdlemd3  37330  cdleme7aa  37372  cdleme7b  37374  cdleme7c  37375  cdleme7d  37376  cdleme7ga  37378  cdleme16aN  37389  cdleme11dN  37392  cdleme11e  37393  cdleme11l  37399  cdleme11  37400  cdleme12  37401  cdleme14  37403  cdleme15c  37406  cdleme16b  37409  cdleme16d  37411  cdleme17b  37417  cdleme17c  37418  cdleme18c  37423  cdleme18d  37425  cdlemeda  37428  cdlemednpq  37429  cdleme19a  37433  cdleme19c  37435  cdleme20aN  37439  cdleme20bN  37440  cdleme20d  37442  cdleme20f  37444  cdleme20g  37445  cdleme20j  37448  cdleme20l1  37450  cdleme21f  37462  cdleme22aa  37469  cdleme22a  37470  cdleme22cN  37472  cdleme22e  37474  cdleme22f2  37477  cdleme22g  37478  cdleme23b  37480  cdleme23c  37481  cdleme26e  37489  cdleme26fALTN  37492  cdleme26f  37493  cdleme26f2ALTN  37494  cdleme26f2  37495  cdleme28a  37500  cdleme28b  37501  cdleme32b  37572  cdleme32c  37573  cdleme32e  37575  cdleme35h2  37587  cdleme38m  37593  cdleme41sn4aw  37605  cdlemf1  37691  cdlemg1cex  37718  cdlemg2ce  37722  cdlemg4d  37743  cdlemg4f  37745  cdlemg7fvN  37754  cdlemg8a  37757  cdlemg8b  37758  cdlemg8c  37759  cdlemg9a  37762  cdlemg11a  37767  cdlemg11aq  37768  cdlemg10a  37770  cdlemg11b  37772  cdlemg12a  37773  cdlemg12b  37774  cdlemg12d  37776  cdlemg12e  37777  cdlemg12f  37778  cdlemg12g  37779  cdlemg12  37780  cdlemg13a  37781  cdlemg13  37782  cdlemg14f  37783  cdlemg14g  37784  cdlemg17b  37792  cdlemg17dN  37793  cdlemg17e  37795  cdlemg17h  37798  cdlemg17pq  37802  cdlemg17iqN  37804  cdlemg18b  37809  cdlemg18c  37810  cdlemg18d  37811  cdlemg18  37812  cdlemg19  37814  cdlemg21  37816  cdlemg27a  37822  cdlemg31b0N  37824  cdlemg27b  37826  cdlemg33b0  37831  cdlemg33c0  37832  cdlemg28  37834  cdlemg33a  37836  cdlemg35  37843  cdlemg42  37859  cdlemg44a  37861  cdlemg47  37866  cdlemh2  37946  cdlemh  37947  cdlemj1  37951  cdlemk3  37963  cdlemk5  37966  cdlemki  37971  cdlemksv2  37977  cdlemk7  37978  cdlemk11  37979  cdlemk12  37980  cdlemkole  37983  cdlemk14  37984  cdlemk15  37985  cdlemk16a  37986  cdlemk16  37987  cdlemkj  37993  cdlemkuv2  37997  cdlemk18  37998  cdlemk19  37999  cdlemk7u  38000  cdlemk12u  38002  cdlemkoatnle-2N  38005  cdlemk13-2N  38006  cdlemkole-2N  38007  cdlemk14-2N  38008  cdlemk15-2N  38009  cdlemk16-2N  38010  cdlemk17-2N  38011  cdlemk18-2N  38016  cdlemk19-2N  38017  cdlemk7u-2N  38018  cdlemk11u-2N  38019  cdlemk12u-2N  38020  cdlemk21-2N  38021  cdlemk20-2N  38022  cdlemk22  38023  cdlemk30  38024  cdlemk31  38026  cdlemk32  38027  cdlemk24-3  38033  cdlemkid2  38054  cdlemkfid3N  38055  cdlemk45  38077  cdlemk46  38078  cdlemk47  38079  cdlemk52  38084  cdlemk53a  38085  cdleml1N  38106  cdleml3N  38108  cdlemn7  38333  cdlemn10  38336  dihordlem7  38344  dihord1  38348  dihord2a  38349  dihord10  38353  dihord11c  38354  dihord2pre2  38356  hlhilphllem  39089  fmuldfeq  41856