Theorem simp33 1191

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

Syntax hints:   → wi 4   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  simp133  1290  simp233  1299  simp333  1308  smogt  7802  bitsfzo  15638  frlmphl  20621  mdetunilem4  20922  mdetuni0  20928  mdetmul  20930  decpmatmullem  21077  logexprlim  25497  ax5seg  26421  iocinioc2  30255  bnj966  31863  eqfunresadj  32524  cgrtr  32974  cgrtr3  32976  ofscom  32989  segconeq  32992  btwnxfr  33038  colinearxfr  33057  fscgr  33062  btwnconn1lem1  33069  btwnconn1lem2  33070  btwnconn1lem5  33073  btwnconn1lem6  33074  btwnconn1lem8  33076  btwnconn1lem9  33077  btwnconn1lem10  33078  btwnconn1lem11  33079  btwnconn1lem12  33080  brsegle2  33091  seglecgr12im  33092  seglecgr12  33093  segletr  33096  outsideofeq  33112  lshpkrlem5  35695  lshpkrlem6  35696  atbtwnexOLDN  36028  atbtwnex  36029  4noncolr3  36034  3dimlem3a  36041  3dimlem4a  36044  3dim1  36048  3dim2  36049  1cvrat  36057  2atjlej  36060  hlatexch4  36062  ps-2b  36063  2atm  36108  ps-2c  36109  lvolex3N  36119  2atmat  36142  lvolnlelpln  36166  4atlem10  36187  4atlem11b  36189  4atlem11  36190  4at  36194  4at2  36195  2lplnja  36200  2lplnj  36201  dalemclccjdd  36269  paddasslem5  36405  paddasslem15  36415  pmodlem1  36427  dalawlem1  36452  dalawlem3  36454  dalawlem4  36455  dalawlem5  36456  dalawlem6  36457  dalawlem7  36458  dalawlem8  36459  dalawlem9  36460  dalawlem11  36462  dalawlem12  36463  dalawlem15  36466  osumcllem5N  36541  osumcllem6N  36542  lhpexle3lem  36592  lhpmcvr4N  36607  lhpmcvr6N  36609  4atexlemex6  36655  4atex2  36658  4atex2-0bOLDN  36660  4atex3  36662  ltrn11at  36728  cdlemd3  36781  cdleme7aa  36823  cdleme7b  36825  cdleme7c  36826  cdleme7d  36827  cdleme7ga  36829  cdleme16aN  36840  cdleme11dN  36843  cdleme11e  36844  cdleme11l  36850  cdleme11  36851  cdleme12  36852  cdleme14  36854  cdleme15c  36857  cdleme16b  36860  cdleme16d  36862  cdleme17b  36868  cdleme17c  36869  cdleme18c  36874  cdleme18d  36876  cdlemeda  36879  cdlemednpq  36880  cdleme19a  36884  cdleme19c  36886  cdleme20aN  36890  cdleme20bN  36891  cdleme20d  36893  cdleme20f  36895  cdleme20g  36896  cdleme20j  36899  cdleme20l1  36901  cdleme21f  36913  cdleme22aa  36920  cdleme22a  36921  cdleme22cN  36923  cdleme22e  36925  cdleme22f2  36928  cdleme22g  36929  cdleme23b  36931  cdleme23c  36932  cdleme26e  36940  cdleme26fALTN  36943  cdleme26f  36944  cdleme26f2ALTN  36945  cdleme26f2  36946  cdleme28a  36951  cdleme28b  36952  cdleme32b  37023  cdleme32c  37024  cdleme32e  37026  cdleme35h2  37038  cdleme38m  37044  cdleme41sn4aw  37056  cdlemf1  37142  cdlemg1cex  37169  cdlemg2ce  37173  cdlemg4d  37194  cdlemg4f  37196  cdlemg7fvN  37205  cdlemg8a  37208  cdlemg8b  37209  cdlemg8c  37210  cdlemg9a  37213  cdlemg11a  37218  cdlemg11aq  37219  cdlemg10a  37221  cdlemg11b  37223  cdlemg12a  37224  cdlemg12b  37225  cdlemg12d  37227  cdlemg12e  37228  cdlemg12f  37229  cdlemg12g  37230  cdlemg12  37231  cdlemg13a  37232  cdlemg13  37233  cdlemg14f  37234  cdlemg14g  37235  cdlemg17b  37243  cdlemg17dN  37244  cdlemg17e  37246  cdlemg17h  37249  cdlemg17pq  37253  cdlemg17iqN  37255  cdlemg18b  37260  cdlemg18c  37261  cdlemg18d  37262  cdlemg18  37263  cdlemg19  37265  cdlemg21  37267  cdlemg27a  37273  cdlemg31b0N  37275  cdlemg27b  37277  cdlemg33b0  37282  cdlemg33c0  37283  cdlemg28  37285  cdlemg33a  37287  cdlemg35  37294  cdlemg42  37310  cdlemg44a  37312  cdlemg47  37317  cdlemh2  37397  cdlemh  37398  cdlemj1  37402  cdlemk3  37414  cdlemk5  37417  cdlemki  37422  cdlemksv2  37428  cdlemk7  37429  cdlemk11  37430  cdlemk12  37431  cdlemkole  37434  cdlemk14  37435  cdlemk15  37436  cdlemk16a  37437  cdlemk16  37438  cdlemkj  37444  cdlemkuv2  37448  cdlemk18  37449  cdlemk19  37450  cdlemk7u  37451  cdlemk12u  37453  cdlemkoatnle-2N  37456  cdlemk13-2N  37457  cdlemkole-2N  37458  cdlemk14-2N  37459  cdlemk15-2N  37460  cdlemk16-2N  37461  cdlemk17-2N  37462  cdlemk18-2N  37467  cdlemk19-2N  37468  cdlemk7u-2N  37469  cdlemk11u-2N  37470  cdlemk12u-2N  37471  cdlemk21-2N  37472  cdlemk20-2N  37473  cdlemk22  37474  cdlemk30  37475  cdlemk31  37477  cdlemk32  37478  cdlemk24-3  37484  cdlemkid2  37505  cdlemkfid3N  37506  cdlemk45  37528  cdlemk46  37529  cdlemk47  37530  cdlemk52  37535  cdlemk53a  37536  cdleml1N  37557  cdleml3N  37559  cdlemn7  37784  cdlemn10  37787  dihordlem7  37795  dihord1  37799  dihord2a  37800  dihord10  37804  dihord11c  37805  dihord2pre2  37807  hlhilphllem  38540  fmuldfeq  41295