Theorem simp33 1212

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp133  1311  simp233  1320  simp333  1329  eqfunresadj  7317  smogt  8313  bitsfzo  16381  frlmphl  21666  mdetunilem4  22478  mdetuni0  22484  mdetmul  22486  decpmatmullem  22634  logexprlim  27112  noinfres  27610  ax5seg  28841  iocinioc2  32675  bnj966  34907  cgrtr  35953  cgrtr3  35955  ofscom  35968  segconeq  35971  btwnxfr  36017  colinearxfr  36036  fscgr  36041  btwnconn1lem1  36048  btwnconn1lem2  36049  btwnconn1lem5  36052  btwnconn1lem6  36053  btwnconn1lem8  36055  btwnconn1lem9  36056  btwnconn1lem10  36057  btwnconn1lem11  36058  btwnconn1lem12  36059  brsegle2  36070  seglecgr12im  36071  seglecgr12  36072  segletr  36075  outsideofeq  36091  lshpkrlem5  39080  lshpkrlem6  39081  atbtwnexOLDN  39414  atbtwnex  39415  4noncolr3  39420  3dimlem3a  39427  3dimlem4a  39430  3dim1  39434  3dim2  39435  1cvrat  39443  2atjlej  39446  hlatexch4  39448  ps-2b  39449  2atm  39494  ps-2c  39495  lvolex3N  39505  2atmat  39528  lvolnlelpln  39552  4atlem10  39573  4atlem11b  39575  4atlem11  39576  4at  39580  4at2  39581  2lplnja  39586  2lplnj  39587  dalemclccjdd  39655  paddasslem5  39791  paddasslem15  39801  pmodlem1  39813  dalawlem1  39838  dalawlem3  39840  dalawlem4  39841  dalawlem5  39842  dalawlem6  39843  dalawlem7  39844  dalawlem8  39845  dalawlem9  39846  dalawlem11  39848  dalawlem12  39849  dalawlem15  39852  osumcllem5N  39927  osumcllem6N  39928  lhpexle3lem  39978  lhpmcvr4N  39993  lhpmcvr6N  39995  4atexlemex6  40041  4atex2  40044  4atex2-0bOLDN  40046  4atex3  40048  ltrn11at  40114  cdlemd3  40167  cdleme7aa  40209  cdleme7b  40211  cdleme7c  40212  cdleme7d  40213  cdleme7ga  40215  cdleme16aN  40226  cdleme11dN  40229  cdleme11e  40230  cdleme11l  40236  cdleme11  40237  cdleme12  40238  cdleme14  40240  cdleme15c  40243  cdleme16b  40246  cdleme16d  40248  cdleme17b  40254  cdleme17c  40255  cdleme18c  40260  cdleme18d  40262  cdlemeda  40265  cdlemednpq  40266  cdleme19a  40270  cdleme19c  40272  cdleme20aN  40276  cdleme20bN  40277  cdleme20d  40279  cdleme20f  40281  cdleme20g  40282  cdleme20j  40285  cdleme20l1  40287  cdleme21f  40299  cdleme22aa  40306  cdleme22a  40307  cdleme22cN  40309  cdleme22e  40311  cdleme22f2  40314  cdleme22g  40315  cdleme23b  40317  cdleme23c  40318  cdleme26e  40326  cdleme26fALTN  40329  cdleme26f  40330  cdleme26f2ALTN  40331  cdleme26f2  40332  cdleme28a  40337  cdleme28b  40338  cdleme32b  40409  cdleme32c  40410  cdleme32e  40412  cdleme35h2  40424  cdleme38m  40430  cdleme41sn4aw  40442  cdlemf1  40528  cdlemg1cex  40555  cdlemg2ce  40559  cdlemg4d  40580  cdlemg4f  40582  cdlemg7fvN  40591  cdlemg8a  40594  cdlemg8b  40595  cdlemg8c  40596  cdlemg9a  40599  cdlemg11a  40604  cdlemg11aq  40605  cdlemg10a  40607  cdlemg11b  40609  cdlemg12a  40610  cdlemg12b  40611  cdlemg12d  40613  cdlemg12e  40614  cdlemg12f  40615  cdlemg12g  40616  cdlemg12  40617  cdlemg13a  40618  cdlemg13  40619  cdlemg14f  40620  cdlemg14g  40621  cdlemg17b  40629  cdlemg17dN  40630  cdlemg17e  40632  cdlemg17h  40635  cdlemg17pq  40639  cdlemg17iqN  40641  cdlemg18b  40646  cdlemg18c  40647  cdlemg18d  40648  cdlemg18  40649  cdlemg19  40651  cdlemg21  40653  cdlemg27a  40659  cdlemg31b0N  40661  cdlemg27b  40663  cdlemg33b0  40668  cdlemg33c0  40669  cdlemg28  40671  cdlemg33a  40673  cdlemg35  40680  cdlemg42  40696  cdlemg44a  40698  cdlemg47  40703  cdlemh2  40783  cdlemh  40784  cdlemj1  40788  cdlemk3  40800  cdlemk5  40803  cdlemki  40808  cdlemksv2  40814  cdlemk7  40815  cdlemk11  40816  cdlemk12  40817  cdlemkole  40820  cdlemk14  40821  cdlemk15  40822  cdlemk16a  40823  cdlemk16  40824  cdlemkj  40830  cdlemkuv2  40834  cdlemk18  40835  cdlemk19  40836  cdlemk7u  40837  cdlemk12u  40839  cdlemkoatnle-2N  40842  cdlemk13-2N  40843  cdlemkole-2N  40844  cdlemk14-2N  40845  cdlemk15-2N  40846  cdlemk16-2N  40847  cdlemk17-2N  40848  cdlemk18-2N  40853  cdlemk19-2N  40854  cdlemk7u-2N  40855  cdlemk11u-2N  40856  cdlemk12u-2N  40857  cdlemk21-2N  40858  cdlemk20-2N  40859  cdlemk22  40860  cdlemk30  40861  cdlemk31  40863  cdlemk32  40864  cdlemk24-3  40870  cdlemkid2  40891  cdlemkfid3N  40892  cdlemk45  40914  cdlemk46  40915  cdlemk47  40916  cdlemk52  40921  cdlemk53a  40922  cdleml1N  40943  cdleml3N  40945  cdlemn7  41170  cdlemn10  41173  dihordlem7  41181  dihord1  41185  dihord2a  41186  dihord10  41190  dihord11c  41191  dihord2pre2  41193  hlhilphllem  41926  fmuldfeq  45554  usgrgrtrirex  47922  seposep  48887  iscnrm3rlem8  48908  iscnrm3llem2  48911