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  7301  smogt  8297  bitsfzo  16365  frlmphl  21707  mdetunilem4  22519  mdetuni0  22525  mdetmul  22527  decpmatmullem  22675  logexprlim  27153  noinfres  27651  ax5seg  28902  iocinioc2  32741  bnj966  34930  cgrtr  35985  cgrtr3  35987  ofscom  36000  segconeq  36003  btwnxfr  36049  colinearxfr  36068  fscgr  36073  btwnconn1lem1  36080  btwnconn1lem2  36081  btwnconn1lem5  36084  btwnconn1lem6  36085  btwnconn1lem8  36087  btwnconn1lem9  36088  btwnconn1lem10  36089  btwnconn1lem11  36090  btwnconn1lem12  36091  brsegle2  36102  seglecgr12im  36103  seglecgr12  36104  segletr  36107  outsideofeq  36123  lshpkrlem5  39112  lshpkrlem6  39113  atbtwnexOLDN  39446  atbtwnex  39447  4noncolr3  39452  3dimlem3a  39459  3dimlem4a  39462  3dim1  39466  3dim2  39467  1cvrat  39475  2atjlej  39478  hlatexch4  39480  ps-2b  39481  2atm  39526  ps-2c  39527  lvolex3N  39537  2atmat  39560  lvolnlelpln  39584  4atlem10  39605  4atlem11b  39607  4atlem11  39608  4at  39612  4at2  39613  2lplnja  39618  2lplnj  39619  dalemclccjdd  39687  paddasslem5  39823  paddasslem15  39833  pmodlem1  39845  dalawlem1  39870  dalawlem3  39872  dalawlem4  39873  dalawlem5  39874  dalawlem6  39875  dalawlem7  39876  dalawlem8  39877  dalawlem9  39878  dalawlem11  39880  dalawlem12  39881  dalawlem15  39884  osumcllem5N  39959  osumcllem6N  39960  lhpexle3lem  40010  lhpmcvr4N  40025  lhpmcvr6N  40027  4atexlemex6  40073  4atex2  40076  4atex2-0bOLDN  40078  4atex3  40080  ltrn11at  40146  cdlemd3  40199  cdleme7aa  40241  cdleme7b  40243  cdleme7c  40244  cdleme7d  40245  cdleme7ga  40247  cdleme16aN  40258  cdleme11dN  40261  cdleme11e  40262  cdleme11l  40268  cdleme11  40269  cdleme12  40270  cdleme14  40272  cdleme15c  40275  cdleme16b  40278  cdleme16d  40280  cdleme17b  40286  cdleme17c  40287  cdleme18c  40292  cdleme18d  40294  cdlemeda  40297  cdlemednpq  40298  cdleme19a  40302  cdleme19c  40304  cdleme20aN  40308  cdleme20bN  40309  cdleme20d  40311  cdleme20f  40313  cdleme20g  40314  cdleme20j  40317  cdleme20l1  40319  cdleme21f  40331  cdleme22aa  40338  cdleme22a  40339  cdleme22cN  40341  cdleme22e  40343  cdleme22f2  40346  cdleme22g  40347  cdleme23b  40349  cdleme23c  40350  cdleme26e  40358  cdleme26fALTN  40361  cdleme26f  40362  cdleme26f2ALTN  40363  cdleme26f2  40364  cdleme28a  40369  cdleme28b  40370  cdleme32b  40441  cdleme32c  40442  cdleme32e  40444  cdleme35h2  40456  cdleme38m  40462  cdleme41sn4aw  40474  cdlemf1  40560  cdlemg1cex  40587  cdlemg2ce  40591  cdlemg4d  40612  cdlemg4f  40614  cdlemg7fvN  40623  cdlemg8a  40626  cdlemg8b  40627  cdlemg8c  40628  cdlemg9a  40631  cdlemg11a  40636  cdlemg11aq  40637  cdlemg10a  40639  cdlemg11b  40641  cdlemg12a  40642  cdlemg12b  40643  cdlemg12d  40645  cdlemg12e  40646  cdlemg12f  40647  cdlemg12g  40648  cdlemg12  40649  cdlemg13a  40650  cdlemg13  40651  cdlemg14f  40652  cdlemg14g  40653  cdlemg17b  40661  cdlemg17dN  40662  cdlemg17e  40664  cdlemg17h  40667  cdlemg17pq  40671  cdlemg17iqN  40673  cdlemg18b  40678  cdlemg18c  40679  cdlemg18d  40680  cdlemg18  40681  cdlemg19  40683  cdlemg21  40685  cdlemg27a  40691  cdlemg31b0N  40693  cdlemg27b  40695  cdlemg33b0  40700  cdlemg33c0  40701  cdlemg28  40703  cdlemg33a  40705  cdlemg35  40712  cdlemg42  40728  cdlemg44a  40730  cdlemg47  40735  cdlemh2  40815  cdlemh  40816  cdlemj1  40820  cdlemk3  40832  cdlemk5  40835  cdlemki  40840  cdlemksv2  40846  cdlemk7  40847  cdlemk11  40848  cdlemk12  40849  cdlemkole  40852  cdlemk14  40853  cdlemk15  40854  cdlemk16a  40855  cdlemk16  40856  cdlemkj  40862  cdlemkuv2  40866  cdlemk18  40867  cdlemk19  40868  cdlemk7u  40869  cdlemk12u  40871  cdlemkoatnle-2N  40874  cdlemk13-2N  40875  cdlemkole-2N  40876  cdlemk14-2N  40877  cdlemk15-2N  40878  cdlemk16-2N  40879  cdlemk17-2N  40880  cdlemk18-2N  40885  cdlemk19-2N  40886  cdlemk7u-2N  40887  cdlemk11u-2N  40888  cdlemk12u-2N  40889  cdlemk21-2N  40890  cdlemk20-2N  40891  cdlemk22  40892  cdlemk30  40893  cdlemk31  40895  cdlemk32  40896  cdlemk24-3  40902  cdlemkid2  40923  cdlemkfid3N  40924  cdlemk45  40946  cdlemk46  40947  cdlemk47  40948  cdlemk52  40953  cdlemk53a  40954  cdleml1N  40975  cdleml3N  40977  cdlemn7  41202  cdlemn10  41205  dihordlem7  41213  dihord1  41217  dihord2a  41218  dihord10  41222  dihord11c  41223  dihord2pre2  41225  hlhilphllem  41958  fmuldfeq  45584  usgrgrtrirex  47954  grlimprclnbgredg  48001  seposep  48930  iscnrm3rlem8  48951  iscnrm3llem2  48954