Theorem simp33 1230

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp133  1329  simp233  1338  simp333  1347  eqfunresadj  7368  smogt  8368  bitsfzo  16598  frlmphl  22080  mdetunilem4  22923  mdetuni0  22929  mdetmul  22931  decpmatmullem  23082  logexprlim  27545  noinfres  28072  ax5seg  29509  iocinioc2  33364  bnj966  35567  cgrtr  36737  cgrtr3  36739  ofscom  36752  segconeq  36755  btwnxfr  36801  colinearxfr  36820  fscgr  36825  btwnconn1lem1  36832  btwnconn1lem2  36833  btwnconn1lem5  36836  btwnconn1lem6  36837  btwnconn1lem8  36839  btwnconn1lem9  36840  btwnconn1lem10  36841  btwnconn1lem11  36842  btwnconn1lem12  36843  brsegle2  36854  seglecgr12im  36855  seglecgr12  36856  segletr  36859  outsideofeq  36875  lshpkrlem5  40151  lshpkrlem6  40152  atbtwnexOLDN  40484  atbtwnex  40485  4noncolr3  40490  3dimlem3a  40497  3dimlem4a  40500  3dim1  40504  3dim2  40505  1cvrat  40513  2atjlej  40516  hlatexch4  40518  ps-2b  40519  2atm  40564  ps-2c  40565  lvolex3N  40575  2atmat  40598  lvolnlelpln  40622  4atlem10  40643  4atlem11b  40645  4atlem11  40646  4at  40650  4at2  40651  2lplnja  40656  2lplnj  40657  dalemclccjdd  40725  paddasslem5  40861  paddasslem15  40871  pmodlem1  40883  dalawlem1  40908  dalawlem3  40910  dalawlem4  40911  dalawlem5  40912  dalawlem6  40913  dalawlem7  40914  dalawlem8  40915  dalawlem9  40916  dalawlem11  40918  dalawlem12  40919  dalawlem15  40922  osumcllem5N  40997  osumcllem6N  40998  lhpexle3lem  41048  lhpmcvr4N  41063  lhpmcvr6N  41065  4atexlemex6  41111  4atex2  41114  4atex2-0bOLDN  41116  4atex3  41118  ltrn11at  41184  cdlemd3  41237  cdleme7aa  41279  cdleme7b  41281  cdleme7c  41282  cdleme7d  41283  cdleme7ga  41285  cdleme16aN  41296  cdleme11dN  41299  cdleme11e  41300  cdleme11l  41306  cdleme11  41307  cdleme12  41308  cdleme14  41310  cdleme15c  41313  cdleme16b  41316  cdleme16d  41318  cdleme17b  41324  cdleme17c  41325  cdleme18c  41330  cdleme18d  41332  cdlemeda  41335  cdlemednpq  41336  cdleme19a  41340  cdleme19c  41342  cdleme20aN  41346  cdleme20bN  41347  cdleme20d  41349  cdleme20f  41351  cdleme20g  41352  cdleme20j  41355  cdleme20l1  41357  cdleme21f  41369  cdleme22aa  41376  cdleme22a  41377  cdleme22cN  41379  cdleme22e  41381  cdleme22f2  41384  cdleme22g  41385  cdleme23b  41387  cdleme23c  41388  cdleme26e  41396  cdleme26fALTN  41399  cdleme26f  41400  cdleme26f2ALTN  41401  cdleme26f2  41402  cdleme28a  41407  cdleme28b  41408  cdleme32b  41479  cdleme32c  41480  cdleme32e  41482  cdleme35h2  41494  cdleme38m  41500  cdleme41sn4aw  41512  cdlemf1  41598  cdlemg1cex  41625  cdlemg2ce  41629  cdlemg4d  41650  cdlemg4f  41652  cdlemg7fvN  41661  cdlemg8a  41664  cdlemg8b  41665  cdlemg8c  41666  cdlemg9a  41669  cdlemg11a  41674  cdlemg11aq  41675  cdlemg10a  41677  cdlemg11b  41679  cdlemg12a  41680  cdlemg12b  41681  cdlemg12d  41683  cdlemg12e  41684  cdlemg12f  41685  cdlemg12g  41686  cdlemg12  41687  cdlemg13a  41688  cdlemg13  41689  cdlemg14f  41690  cdlemg14g  41691  cdlemg17b  41699  cdlemg17dN  41700  cdlemg17e  41702  cdlemg17h  41705  cdlemg17pq  41709  cdlemg17iqN  41711  cdlemg18b  41716  cdlemg18c  41717  cdlemg18d  41718  cdlemg18  41719  cdlemg19  41721  cdlemg21  41723  cdlemg27a  41729  cdlemg31b0N  41731  cdlemg27b  41733  cdlemg33b0  41738  cdlemg33c0  41739  cdlemg28  41741  cdlemg33a  41743  cdlemg35  41750  cdlemg42  41766  cdlemg44a  41768  cdlemg47  41773  cdlemh2  41853  cdlemh  41854  cdlemj1  41858  cdlemk3  41870  cdlemk5  41873  cdlemki  41878  cdlemksv2  41884  cdlemk7  41885  cdlemk11  41886  cdlemk12  41887  cdlemkole  41890  cdlemk14  41891  cdlemk15  41892  cdlemk16a  41893  cdlemk16  41894  cdlemkj  41900  cdlemkuv2  41904  cdlemk18  41905  cdlemk19  41906  cdlemk7u  41907  cdlemk12u  41909  cdlemkoatnle-2N  41912  cdlemk13-2N  41913  cdlemkole-2N  41914  cdlemk14-2N  41915  cdlemk15-2N  41916  cdlemk16-2N  41917  cdlemk17-2N  41918  cdlemk18-2N  41923  cdlemk19-2N  41924  cdlemk7u-2N  41925  cdlemk11u-2N  41926  cdlemk12u-2N  41927  cdlemk21-2N  41928  cdlemk20-2N  41929  cdlemk22  41930  cdlemk30  41931  cdlemk31  41933  cdlemk32  41934  cdlemk24-3  41940  cdlemkid2  41961  cdlemkfid3N  41962  cdlemk45  41984  cdlemk46  41985  cdlemk47  41986  cdlemk52  41991  cdlemk53a  41992  cdleml1N  42013  cdleml3N  42015  cdlemn7  42240  cdlemn10  42243  dihordlem7  42251  dihord1  42255  dihord2a  42256  dihord10  42260  dihord11c  42261  dihord2pre2  42263  hlhilphllem  42996  fmuldfeq  46564  usgrgrtrirex  49017  grlimprclnbgredg  49064  seposep  50003  iscnrm3rlem8  50024  iscnrm3llem2  50027