Theorem simp33 1210

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 1137	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜏)
2	1	3ad2ant3 1134	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp133  1309  simp233  1318  simp333  1327  smogt  8247  bitsfzo  16221  frlmphl  21071  mdetunilem4  21847  mdetuni0  21853  mdetmul  21855  decpmatmullem  22003  logexprlim  26456  ax5seg  27442  iocinioc2  31235  bnj966  33063  eqfunresadj  33868  noinfres  33999  cgrtr  34368  cgrtr3  34370  ofscom  34383  segconeq  34386  btwnxfr  34432  colinearxfr  34451  fscgr  34456  btwnconn1lem1  34463  btwnconn1lem2  34464  btwnconn1lem5  34467  btwnconn1lem6  34468  btwnconn1lem8  34470  btwnconn1lem9  34471  btwnconn1lem10  34472  btwnconn1lem11  34473  btwnconn1lem12  34474  brsegle2  34485  seglecgr12im  34486  seglecgr12  34487  segletr  34490  outsideofeq  34506  lshpkrlem5  37348  lshpkrlem6  37349  atbtwnexOLDN  37682  atbtwnex  37683  4noncolr3  37688  3dimlem3a  37695  3dimlem4a  37698  3dim1  37702  3dim2  37703  1cvrat  37711  2atjlej  37714  hlatexch4  37716  ps-2b  37717  2atm  37762  ps-2c  37763  lvolex3N  37773  2atmat  37796  lvolnlelpln  37820  4atlem10  37841  4atlem11b  37843  4atlem11  37844  4at  37848  4at2  37849  2lplnja  37854  2lplnj  37855  dalemclccjdd  37923  paddasslem5  38059  paddasslem15  38069  pmodlem1  38081  dalawlem1  38106  dalawlem3  38108  dalawlem4  38109  dalawlem5  38110  dalawlem6  38111  dalawlem7  38112  dalawlem8  38113  dalawlem9  38114  dalawlem11  38116  dalawlem12  38117  dalawlem15  38120  osumcllem5N  38195  osumcllem6N  38196  lhpexle3lem  38246  lhpmcvr4N  38261  lhpmcvr6N  38263  4atexlemex6  38309  4atex2  38312  4atex2-0bOLDN  38314  4atex3  38316  ltrn11at  38382  cdlemd3  38435  cdleme7aa  38477  cdleme7b  38479  cdleme7c  38480  cdleme7d  38481  cdleme7ga  38483  cdleme16aN  38494  cdleme11dN  38497  cdleme11e  38498  cdleme11l  38504  cdleme11  38505  cdleme12  38506  cdleme14  38508  cdleme15c  38511  cdleme16b  38514  cdleme16d  38516  cdleme17b  38522  cdleme17c  38523  cdleme18c  38528  cdleme18d  38530  cdlemeda  38533  cdlemednpq  38534  cdleme19a  38538  cdleme19c  38540  cdleme20aN  38544  cdleme20bN  38545  cdleme20d  38547  cdleme20f  38549  cdleme20g  38550  cdleme20j  38553  cdleme20l1  38555  cdleme21f  38567  cdleme22aa  38574  cdleme22a  38575  cdleme22cN  38577  cdleme22e  38579  cdleme22f2  38582  cdleme22g  38583  cdleme23b  38585  cdleme23c  38586  cdleme26e  38594  cdleme26fALTN  38597  cdleme26f  38598  cdleme26f2ALTN  38599  cdleme26f2  38600  cdleme28a  38605  cdleme28b  38606  cdleme32b  38677  cdleme32c  38678  cdleme32e  38680  cdleme35h2  38692  cdleme38m  38698  cdleme41sn4aw  38710  cdlemf1  38796  cdlemg1cex  38823  cdlemg2ce  38827  cdlemg4d  38848  cdlemg4f  38850  cdlemg7fvN  38859  cdlemg8a  38862  cdlemg8b  38863  cdlemg8c  38864  cdlemg9a  38867  cdlemg11a  38872  cdlemg11aq  38873  cdlemg10a  38875  cdlemg11b  38877  cdlemg12a  38878  cdlemg12b  38879  cdlemg12d  38881  cdlemg12e  38882  cdlemg12f  38883  cdlemg12g  38884  cdlemg12  38885  cdlemg13a  38886  cdlemg13  38887  cdlemg14f  38888  cdlemg14g  38889  cdlemg17b  38897  cdlemg17dN  38898  cdlemg17e  38900  cdlemg17h  38903  cdlemg17pq  38907  cdlemg17iqN  38909  cdlemg18b  38914  cdlemg18c  38915  cdlemg18d  38916  cdlemg18  38917  cdlemg19  38919  cdlemg21  38921  cdlemg27a  38927  cdlemg31b0N  38929  cdlemg27b  38931  cdlemg33b0  38936  cdlemg33c0  38937  cdlemg28  38939  cdlemg33a  38941  cdlemg35  38948  cdlemg42  38964  cdlemg44a  38966  cdlemg47  38971  cdlemh2  39051  cdlemh  39052  cdlemj1  39056  cdlemk3  39068  cdlemk5  39071  cdlemki  39076  cdlemksv2  39082  cdlemk7  39083  cdlemk11  39084  cdlemk12  39085  cdlemkole  39088  cdlemk14  39089  cdlemk15  39090  cdlemk16a  39091  cdlemk16  39092  cdlemkj  39098  cdlemkuv2  39102  cdlemk18  39103  cdlemk19  39104  cdlemk7u  39105  cdlemk12u  39107  cdlemkoatnle-2N  39110  cdlemk13-2N  39111  cdlemkole-2N  39112  cdlemk14-2N  39113  cdlemk15-2N  39114  cdlemk16-2N  39115  cdlemk17-2N  39116  cdlemk18-2N  39121  cdlemk19-2N  39122  cdlemk7u-2N  39123  cdlemk11u-2N  39124  cdlemk12u-2N  39125  cdlemk21-2N  39126  cdlemk20-2N  39127  cdlemk22  39128  cdlemk30  39129  cdlemk31  39131  cdlemk32  39132  cdlemk24-3  39138  cdlemkid2  39159  cdlemkfid3N  39160  cdlemk45  39182  cdlemk46  39183  cdlemk47  39184  cdlemk52  39189  cdlemk53a  39190  cdleml1N  39211  cdleml3N  39213  cdlemn7  39438  cdlemn10  39441  dihordlem7  39449  dihord1  39453  dihord2a  39454  dihord10  39458  dihord11c  39459  dihord2pre2  39461  hlhilphllem  40198  fmuldfeq  43374  seposep  46484  iscnrm3rlem8  46506  iscnrm3llem2  46509