Theorem simp31 1208

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp31	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒)

Proof of Theorem simp31

Step	Hyp	Ref	Expression
1		simp1 1135	. 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:  simp131  1307  simp231  1316  simp331  1325  smogt  8246  frlmphl  21068  mdetuni0  21850  mdetmul  21852  gsummatr01lem3  21886  decpmatmullem  22000  tsmsxp  23386  log2sumbnd  26772  ax5seg  27439  wlkoniswlk  28161  iocinioc2  31231  totprob  32530  eqfunresadj  33864  nosupres  33980  noinfres  33995  cgrtr  34364  cgrtr3  34366  ofscom  34379  cgrextend  34380  segconeq  34382  ifscgr  34416  btwnxfr  34428  colinearxfr  34447  brofs2  34449  brifs2  34450  fscgr  34452  btwnconn1lem1  34459  btwnconn1lem2  34460  btwnconn1lem5  34463  btwnconn1lem6  34464  btwnconn1lem7  34465  btwnconn1lem8  34466  btwnconn1lem9  34467  btwnconn1lem10  34468  btwnconn1lem11  34469  btwnconn1lem12  34470  seglecgr12im  34482  seglecgr12  34483  segletr  34486  outsideofeq  34502  ivthALT  34594  lshpkrlem5  37353  lshpkrlem6  37354  exatleN  37644  atbtwn  37686  atbtwnexOLDN  37687  atbtwnex  37688  4noncolr3  37693  3dimlem3a  37700  3dimlem4a  37703  3dim1  37707  3dim2  37708  1cvrat  37716  2atjlej  37719  hlatexch4  37721  ps-2b  37722  2atm  37767  2atmat  37801  4atlem11b  37848  4atlem11  37849  4at  37853  4at2  37854  2lplnja  37859  2lplnj  37860  dalemswapyz  37896  dalemccnedd  37927  cdlemb  38034  paddasslem5  38064  paddasslem15  38074  pmodlem1  38086  dalawlem1  38111  dalawlem3  38113  dalawlem4  38114  dalawlem5  38115  dalawlem6  38116  dalawlem7  38117  dalawlem8  38118  dalawlem9  38119  dalawlem11  38121  dalawlem12  38122  dalawlem15  38125  osumcllem5N  38200  osumcllem6N  38201  lhpexle3lem  38251  lhpmcvr4N  38266  lhpmcvr6N  38268  4atex2  38317  4atex2-0bOLDN  38319  4atex3  38321  ltrn11at  38387  trlval3  38427  cdlemd3  38440  cdleme0moN  38465  cdleme7aa  38482  cdleme7b  38484  cdleme7c  38485  cdleme7d  38486  cdleme7e  38487  cdleme7ga  38488  cdleme7  38489  cdleme16aN  38499  cdleme11dN  38502  cdleme11e  38503  cdleme11l  38509  cdleme11  38510  cdleme12  38511  cdleme14  38513  cdleme15b  38515  cdleme15c  38516  cdleme16b  38519  cdleme16c  38520  cdleme16d  38521  cdleme16e  38522  cdleme16f  38523  cdleme17c  38528  cdleme18c  38533  cdleme18d  38535  cdlemeda  38538  cdleme19a  38543  cdleme19b  38544  cdleme19c  38545  cdleme20aN  38549  cdleme20bN  38550  cdleme20d  38552  cdleme20i  38557  cdleme20j  38558  cdleme20l1  38560  cdleme20l2  38561  cdleme21d  38570  cdleme21e  38571  cdleme21f  38572  cdleme22aa  38579  cdleme22e  38584  cdleme22eALTN  38585  cdleme22f2  38587  cdleme22g  38588  cdleme23b  38590  cdleme26eALTN  38601  cdleme26fALTN  38602  cdleme26f  38603  cdleme26f2ALTN  38604  cdleme26f2  38605  cdleme28a  38610  cdleme28b  38611  cdleme32b  38682  cdleme32c  38683  cdleme32e  38685  cdleme35h  38696  cdleme35sn2aw  38698  cdleme41sn3aw  38714  cdleme41sn4aw  38715  cdlemeg46gfre  38772  cdlemf1  38801  cdlemg1cex  38828  cdlemg2ce  38832  cdlemg4d  38853  cdlemg4e  38854  cdlemg4f  38855  cdlemg4  38857  cdlemg6d  38861  cdlemg6e  38862  cdlemg7fvN  38864  cdlemg8b  38868  cdlemg8c  38869  cdlemg9a  38872  cdlemg9b  38873  cdlemg9  38874  cdlemg11aq  38878  cdlemg10a  38880  cdlemg12a  38883  cdlemg12b  38884  cdlemg12c  38885  cdlemg12d  38886  cdlemg13  38892  cdlemg14f  38893  cdlemg14g  38894  cdlemg17b  38902  cdlemg17dN  38903  cdlemg17e  38905  cdlemg17i  38909  cdlemg17pq  38912  cdlemg17iqN  38914  cdlemg18c  38920  cdlemg18d  38921  cdlemg18  38922  cdlemg19  38924  cdlemg21  38926  cdlemg27a  38932  cdlemg31b0N  38934  cdlemg27b  38936  cdlemg31c  38939  cdlemg33b0  38941  cdlemg33c0  38942  cdlemg33  38951  cdlemg35  38953  cdlemg43  38970  cdlemg44a  38971  cdlemg46  38975  cdlemh2  39056  cdlemh  39057  cdlemj1  39061  cdlemk3  39073  cdlemk5  39076  cdlemk6  39077  cdlemki  39081  cdlemksv2  39087  cdlemk12  39090  cdlemk15  39095  cdlemk16  39097  cdlemk18  39108  cdlemk19  39109  cdlemk7u  39110  cdlemk12u  39112  cdlemkoatnle-2N  39115  cdlemk13-2N  39116  cdlemkole-2N  39117  cdlemk14-2N  39118  cdlemk15-2N  39119  cdlemk16-2N  39120  cdlemk17-2N  39121  cdlemk18-2N  39126  cdlemk19-2N  39127  cdlemk7u-2N  39128  cdlemk11u-2N  39129  cdlemk12u-2N  39130  cdlemk20-2N  39132  cdlemk22  39133  cdlemk30  39134  cdlemk31  39136  cdlemk24-3  39143  cdlemkid2  39164  cdlemkfid3N  39165  cdlemk11ta  39169  cdlemkid3N  39173  cdlemk11tc  39185  cdlemk45  39187  cdlemk46  39188  cdlemk47  39189  cdlemk52  39194  cdlemk53a  39195  cdlemk53b  39196  cdleml1N  39216  cdleml3N  39218  cdlemn7  39443  cdlemn10  39446  dihordlem7  39454  dihord1  39458  dihord11c  39464  dihord2  39467  hlhilphllem  40203  fmuldfeq  43379  seposep  46489  iscnrm3rlem8  46511  iscnrm3llem2  46514