Theorem simp33 1230

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp133  1329  simp233  1338  simp333  1347  eqfunresadj  7363  smogt  8356  bitsfzo  16525  frlmphl  21994  mdetunilem4  22837  mdetuni0  22843  mdetmul  22845  decpmatmullem  22996  logexprlim  27461  noinfres  27958  ax5seg  29395  iocinioc2  33250  bnj966  35453  cgrtr  36572  cgrtr3  36574  ofscom  36587  segconeq  36590  btwnxfr  36636  colinearxfr  36655  fscgr  36660  btwnconn1lem1  36667  btwnconn1lem2  36668  btwnconn1lem5  36671  btwnconn1lem6  36672  btwnconn1lem8  36674  btwnconn1lem9  36675  btwnconn1lem10  36676  btwnconn1lem11  36677  btwnconn1lem12  36678  brsegle2  36689  seglecgr12im  36690  seglecgr12  36691  segletr  36694  outsideofeq  36710  lshpkrlem5  39987  lshpkrlem6  39988  atbtwnexOLDN  40320  atbtwnex  40321  4noncolr3  40326  3dimlem3a  40333  3dimlem4a  40336  3dim1  40340  3dim2  40341  1cvrat  40349  2atjlej  40352  hlatexch4  40354  ps-2b  40355  2atm  40400  ps-2c  40401  lvolex3N  40411  2atmat  40434  lvolnlelpln  40458  4atlem10  40479  4atlem11b  40481  4atlem11  40482  4at  40486  4at2  40487  2lplnja  40492  2lplnj  40493  dalemclccjdd  40561  paddasslem5  40697  paddasslem15  40707  pmodlem1  40719  dalawlem1  40744  dalawlem3  40746  dalawlem4  40747  dalawlem5  40748  dalawlem6  40749  dalawlem7  40750  dalawlem8  40751  dalawlem9  40752  dalawlem11  40754  dalawlem12  40755  dalawlem15  40758  osumcllem5N  40833  osumcllem6N  40834  lhpexle3lem  40884  lhpmcvr4N  40899  lhpmcvr6N  40901  4atexlemex6  40947  4atex2  40950  4atex2-0bOLDN  40952  4atex3  40954  ltrn11at  41020  cdlemd3  41073  cdleme7aa  41115  cdleme7b  41117  cdleme7c  41118  cdleme7d  41119  cdleme7ga  41121  cdleme16aN  41132  cdleme11dN  41135  cdleme11e  41136  cdleme11l  41142  cdleme11  41143  cdleme12  41144  cdleme14  41146  cdleme15c  41149  cdleme16b  41152  cdleme16d  41154  cdleme17b  41160  cdleme17c  41161  cdleme18c  41166  cdleme18d  41168  cdlemeda  41171  cdlemednpq  41172  cdleme19a  41176  cdleme19c  41178  cdleme20aN  41182  cdleme20bN  41183  cdleme20d  41185  cdleme20f  41187  cdleme20g  41188  cdleme20j  41191  cdleme20l1  41193  cdleme21f  41205  cdleme22aa  41212  cdleme22a  41213  cdleme22cN  41215  cdleme22e  41217  cdleme22f2  41220  cdleme22g  41221  cdleme23b  41223  cdleme23c  41224  cdleme26e  41232  cdleme26fALTN  41235  cdleme26f  41236  cdleme26f2ALTN  41237  cdleme26f2  41238  cdleme28a  41243  cdleme28b  41244  cdleme32b  41315  cdleme32c  41316  cdleme32e  41318  cdleme35h2  41330  cdleme38m  41336  cdleme41sn4aw  41348  cdlemf1  41434  cdlemg1cex  41461  cdlemg2ce  41465  cdlemg4d  41486  cdlemg4f  41488  cdlemg7fvN  41497  cdlemg8a  41500  cdlemg8b  41501  cdlemg8c  41502  cdlemg9a  41505  cdlemg11a  41510  cdlemg11aq  41511  cdlemg10a  41513  cdlemg11b  41515  cdlemg12a  41516  cdlemg12b  41517  cdlemg12d  41519  cdlemg12e  41520  cdlemg12f  41521  cdlemg12g  41522  cdlemg12  41523  cdlemg13a  41524  cdlemg13  41525  cdlemg14f  41526  cdlemg14g  41527  cdlemg17b  41535  cdlemg17dN  41536  cdlemg17e  41538  cdlemg17h  41541  cdlemg17pq  41545  cdlemg17iqN  41547  cdlemg18b  41552  cdlemg18c  41553  cdlemg18d  41554  cdlemg18  41555  cdlemg19  41557  cdlemg21  41559  cdlemg27a  41565  cdlemg31b0N  41567  cdlemg27b  41569  cdlemg33b0  41574  cdlemg33c0  41575  cdlemg28  41577  cdlemg33a  41579  cdlemg35  41586  cdlemg42  41602  cdlemg44a  41604  cdlemg47  41609  cdlemh2  41689  cdlemh  41690  cdlemj1  41694  cdlemk3  41706  cdlemk5  41709  cdlemki  41714  cdlemksv2  41720  cdlemk7  41721  cdlemk11  41722  cdlemk12  41723  cdlemkole  41726  cdlemk14  41727  cdlemk15  41728  cdlemk16a  41729  cdlemk16  41730  cdlemkj  41736  cdlemkuv2  41740  cdlemk18  41741  cdlemk19  41742  cdlemk7u  41743  cdlemk12u  41745  cdlemkoatnle-2N  41748  cdlemk13-2N  41749  cdlemkole-2N  41750  cdlemk14-2N  41751  cdlemk15-2N  41752  cdlemk16-2N  41753  cdlemk17-2N  41754  cdlemk18-2N  41759  cdlemk19-2N  41760  cdlemk7u-2N  41761  cdlemk11u-2N  41762  cdlemk12u-2N  41763  cdlemk21-2N  41764  cdlemk20-2N  41765  cdlemk22  41766  cdlemk30  41767  cdlemk31  41769  cdlemk32  41770  cdlemk24-3  41776  cdlemkid2  41797  cdlemkfid3N  41798  cdlemk45  41820  cdlemk46  41821  cdlemk47  41822  cdlemk52  41827  cdlemk53a  41828  cdleml1N  41849  cdleml3N  41851  cdlemn7  42076  cdlemn10  42079  dihordlem7  42087  dihord1  42091  dihord2a  42092  dihord10  42096  dihord11c  42097  dihord2pre2  42099  hlhilphllem  42832  fmuldfeq  46413  usgrgrtrirex  48866  grlimprclnbgredg  48913  seposep  49852  iscnrm3rlem8  49873  iscnrm3llem2  49876