Theorem simp33 1209

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 1087

This theorem is referenced by:  simp133  1308  simp233  1317  simp333  1326  eqfunresadj  7361  smogt  8371  bitsfzo  16382  frlmphl  21557  mdetunilem4  22339  mdetuni0  22345  mdetmul  22347  decpmatmullem  22495  logexprlim  26962  noinfres  27459  ax5seg  28461  iocinioc2  32255  bnj966  34251  cgrtr  35266  cgrtr3  35268  ofscom  35281  segconeq  35284  btwnxfr  35330  colinearxfr  35349  fscgr  35354  btwnconn1lem1  35361  btwnconn1lem2  35362  btwnconn1lem5  35365  btwnconn1lem6  35366  btwnconn1lem8  35368  btwnconn1lem9  35369  btwnconn1lem10  35370  btwnconn1lem11  35371  btwnconn1lem12  35372  brsegle2  35383  seglecgr12im  35384  seglecgr12  35385  segletr  35388  outsideofeq  35404  lshpkrlem5  38289  lshpkrlem6  38290  atbtwnexOLDN  38623  atbtwnex  38624  4noncolr3  38629  3dimlem3a  38636  3dimlem4a  38639  3dim1  38643  3dim2  38644  1cvrat  38652  2atjlej  38655  hlatexch4  38657  ps-2b  38658  2atm  38703  ps-2c  38704  lvolex3N  38714  2atmat  38737  lvolnlelpln  38761  4atlem10  38782  4atlem11b  38784  4atlem11  38785  4at  38789  4at2  38790  2lplnja  38795  2lplnj  38796  dalemclccjdd  38864  paddasslem5  39000  paddasslem15  39010  pmodlem1  39022  dalawlem1  39047  dalawlem3  39049  dalawlem4  39050  dalawlem5  39051  dalawlem6  39052  dalawlem7  39053  dalawlem8  39054  dalawlem9  39055  dalawlem11  39057  dalawlem12  39058  dalawlem15  39061  osumcllem5N  39136  osumcllem6N  39137  lhpexle3lem  39187  lhpmcvr4N  39202  lhpmcvr6N  39204  4atexlemex6  39250  4atex2  39253  4atex2-0bOLDN  39255  4atex3  39257  ltrn11at  39323  cdlemd3  39376  cdleme7aa  39418  cdleme7b  39420  cdleme7c  39421  cdleme7d  39422  cdleme7ga  39424  cdleme16aN  39435  cdleme11dN  39438  cdleme11e  39439  cdleme11l  39445  cdleme11  39446  cdleme12  39447  cdleme14  39449  cdleme15c  39452  cdleme16b  39455  cdleme16d  39457  cdleme17b  39463  cdleme17c  39464  cdleme18c  39469  cdleme18d  39471  cdlemeda  39474  cdlemednpq  39475  cdleme19a  39479  cdleme19c  39481  cdleme20aN  39485  cdleme20bN  39486  cdleme20d  39488  cdleme20f  39490  cdleme20g  39491  cdleme20j  39494  cdleme20l1  39496  cdleme21f  39508  cdleme22aa  39515  cdleme22a  39516  cdleme22cN  39518  cdleme22e  39520  cdleme22f2  39523  cdleme22g  39524  cdleme23b  39526  cdleme23c  39527  cdleme26e  39535  cdleme26fALTN  39538  cdleme26f  39539  cdleme26f2ALTN  39540  cdleme26f2  39541  cdleme28a  39546  cdleme28b  39547  cdleme32b  39618  cdleme32c  39619  cdleme32e  39621  cdleme35h2  39633  cdleme38m  39639  cdleme41sn4aw  39651  cdlemf1  39737  cdlemg1cex  39764  cdlemg2ce  39768  cdlemg4d  39789  cdlemg4f  39791  cdlemg7fvN  39800  cdlemg8a  39803  cdlemg8b  39804  cdlemg8c  39805  cdlemg9a  39808  cdlemg11a  39813  cdlemg11aq  39814  cdlemg10a  39816  cdlemg11b  39818  cdlemg12a  39819  cdlemg12b  39820  cdlemg12d  39822  cdlemg12e  39823  cdlemg12f  39824  cdlemg12g  39825  cdlemg12  39826  cdlemg13a  39827  cdlemg13  39828  cdlemg14f  39829  cdlemg14g  39830  cdlemg17b  39838  cdlemg17dN  39839  cdlemg17e  39841  cdlemg17h  39844  cdlemg17pq  39848  cdlemg17iqN  39850  cdlemg18b  39855  cdlemg18c  39856  cdlemg18d  39857  cdlemg18  39858  cdlemg19  39860  cdlemg21  39862  cdlemg27a  39868  cdlemg31b0N  39870  cdlemg27b  39872  cdlemg33b0  39877  cdlemg33c0  39878  cdlemg28  39880  cdlemg33a  39882  cdlemg35  39889  cdlemg42  39905  cdlemg44a  39907  cdlemg47  39912  cdlemh2  39992  cdlemh  39993  cdlemj1  39997  cdlemk3  40009  cdlemk5  40012  cdlemki  40017  cdlemksv2  40023  cdlemk7  40024  cdlemk11  40025  cdlemk12  40026  cdlemkole  40029  cdlemk14  40030  cdlemk15  40031  cdlemk16a  40032  cdlemk16  40033  cdlemkj  40039  cdlemkuv2  40043  cdlemk18  40044  cdlemk19  40045  cdlemk7u  40046  cdlemk12u  40048  cdlemkoatnle-2N  40051  cdlemk13-2N  40052  cdlemkole-2N  40053  cdlemk14-2N  40054  cdlemk15-2N  40055  cdlemk16-2N  40056  cdlemk17-2N  40057  cdlemk18-2N  40062  cdlemk19-2N  40063  cdlemk7u-2N  40064  cdlemk11u-2N  40065  cdlemk12u-2N  40066  cdlemk21-2N  40067  cdlemk20-2N  40068  cdlemk22  40069  cdlemk30  40070  cdlemk31  40072  cdlemk32  40073  cdlemk24-3  40079  cdlemkid2  40100  cdlemkfid3N  40101  cdlemk45  40123  cdlemk46  40124  cdlemk47  40125  cdlemk52  40130  cdlemk53a  40131  cdleml1N  40152  cdleml3N  40154  cdlemn7  40379  cdlemn10  40382  dihordlem7  40390  dihord1  40394  dihord2a  40395  dihord10  40399  dihord11c  40400  dihord2pre2  40402  hlhilphllem  41139  fmuldfeq  44599  seposep  47647  iscnrm3rlem8  47669  iscnrm3llem2  47672