Theorem simp31 1209

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp131  1308  simp231  1317  simp331  1326  eqfunresadj  7396  smogt  8423  frlmphl  21824  mdetuni0  22648  mdetmul  22650  gsummatr01lem3  22684  decpmatmullem  22798  tsmsxp  24184  log2sumbnd  27606  nosupres  27770  noinfres  27785  ax5seg  28971  wlkoniswlk  29697  iocinioc2  32784  totprob  34392  cgrtr  35956  cgrtr3  35958  ofscom  35971  cgrextend  35972  segconeq  35974  ifscgr  36008  btwnxfr  36020  colinearxfr  36039  brofs2  36041  brifs2  36042  fscgr  36044  btwnconn1lem1  36051  btwnconn1lem2  36052  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem7  36057  btwnconn1lem8  36058  btwnconn1lem9  36059  btwnconn1lem10  36060  btwnconn1lem11  36061  btwnconn1lem12  36062  seglecgr12im  36074  seglecgr12  36075  segletr  36078  outsideofeq  36094  ivthALT  36301  lshpkrlem5  39070  lshpkrlem6  39071  exatleN  39361  atbtwn  39403  atbtwnexOLDN  39404  atbtwnex  39405  4noncolr3  39410  3dimlem3a  39417  3dimlem4a  39420  3dim1  39424  3dim2  39425  1cvrat  39433  2atjlej  39436  hlatexch4  39438  ps-2b  39439  2atm  39484  2atmat  39518  4atlem11b  39565  4atlem11  39566  4at  39570  4at2  39571  2lplnja  39576  2lplnj  39577  dalemswapyz  39613  dalemccnedd  39644  cdlemb  39751  paddasslem5  39781  paddasslem15  39791  pmodlem1  39803  dalawlem1  39828  dalawlem3  39830  dalawlem4  39831  dalawlem5  39832  dalawlem6  39833  dalawlem7  39834  dalawlem8  39835  dalawlem9  39836  dalawlem11  39838  dalawlem12  39839  dalawlem15  39842  osumcllem5N  39917  osumcllem6N  39918  lhpexle3lem  39968  lhpmcvr4N  39983  lhpmcvr6N  39985  4atex2  40034  4atex2-0bOLDN  40036  4atex3  40038  ltrn11at  40104  trlval3  40144  cdlemd3  40157  cdleme0moN  40182  cdleme7aa  40199  cdleme7b  40201  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme16aN  40216  cdleme11dN  40219  cdleme11e  40220  cdleme11l  40226  cdleme11  40227  cdleme12  40228  cdleme14  40230  cdleme15b  40232  cdleme15c  40233  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme16e  40239  cdleme16f  40240  cdleme17c  40245  cdleme18c  40250  cdleme18d  40252  cdlemeda  40255  cdleme19a  40260  cdleme19b  40261  cdleme19c  40262  cdleme20aN  40266  cdleme20bN  40267  cdleme20d  40269  cdleme20i  40274  cdleme20j  40275  cdleme20l1  40277  cdleme20l2  40278  cdleme21d  40287  cdleme21e  40288  cdleme21f  40289  cdleme22aa  40296  cdleme22e  40301  cdleme22eALTN  40302  cdleme22f2  40304  cdleme22g  40305  cdleme23b  40307  cdleme26eALTN  40318  cdleme26fALTN  40319  cdleme26f  40320  cdleme26f2ALTN  40321  cdleme26f2  40322  cdleme28a  40327  cdleme28b  40328  cdleme32b  40399  cdleme32c  40400  cdleme32e  40402  cdleme35h  40413  cdleme35sn2aw  40415  cdleme41sn3aw  40431  cdleme41sn4aw  40432  cdlemeg46gfre  40489  cdlemf1  40518  cdlemg1cex  40545  cdlemg2ce  40549  cdlemg4d  40570  cdlemg4e  40571  cdlemg4f  40572  cdlemg4  40574  cdlemg6d  40578  cdlemg6e  40579  cdlemg7fvN  40581  cdlemg8b  40585  cdlemg8c  40586  cdlemg9a  40589  cdlemg9b  40590  cdlemg9  40591  cdlemg11aq  40595  cdlemg10a  40597  cdlemg12a  40600  cdlemg12b  40601  cdlemg12c  40602  cdlemg12d  40603  cdlemg13  40609  cdlemg14f  40610  cdlemg14g  40611  cdlemg17b  40619  cdlemg17dN  40620  cdlemg17e  40622  cdlemg17i  40626  cdlemg17pq  40629  cdlemg17iqN  40631  cdlemg18c  40637  cdlemg18d  40638  cdlemg18  40639  cdlemg19  40641  cdlemg21  40643  cdlemg27a  40649  cdlemg31b0N  40651  cdlemg27b  40653  cdlemg31c  40656  cdlemg33b0  40658  cdlemg33c0  40659  cdlemg33  40668  cdlemg35  40670  cdlemg43  40687  cdlemg44a  40688  cdlemg46  40692  cdlemh2  40773  cdlemh  40774  cdlemj1  40778  cdlemk3  40790  cdlemk5  40793  cdlemk6  40794  cdlemki  40798  cdlemksv2  40804  cdlemk12  40807  cdlemk15  40812  cdlemk16  40814  cdlemk18  40825  cdlemk19  40826  cdlemk7u  40827  cdlemk12u  40829  cdlemkoatnle-2N  40832  cdlemk13-2N  40833  cdlemkole-2N  40834  cdlemk14-2N  40835  cdlemk15-2N  40836  cdlemk16-2N  40837  cdlemk17-2N  40838  cdlemk18-2N  40843  cdlemk19-2N  40844  cdlemk7u-2N  40845  cdlemk11u-2N  40846  cdlemk12u-2N  40847  cdlemk20-2N  40849  cdlemk22  40850  cdlemk30  40851  cdlemk31  40853  cdlemk24-3  40860  cdlemkid2  40881  cdlemkfid3N  40882  cdlemk11ta  40886  cdlemkid3N  40890  cdlemk11tc  40902  cdlemk45  40904  cdlemk46  40905  cdlemk47  40906  cdlemk52  40911  cdlemk53a  40912  cdlemk53b  40913  cdleml1N  40933  cdleml3N  40935  cdlemn7  41160  cdlemn10  41163  dihordlem7  41171  dihord1  41175  dihord11c  41181  dihord2  41184  hlhilphllem  41920  fmuldfeq  45504  seposep  48605  iscnrm3rlem8  48627  iscnrm3llem2  48630