Theorem simp31 1210

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 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:  simp131  1309  simp231  1318  simp331  1327  eqfunresadj  7352  smogt  8379  frlmphl  21739  mdetuni0  22557  mdetmul  22559  gsummatr01lem3  22593  decpmatmullem  22707  tsmsxp  24091  log2sumbnd  27505  nosupres  27669  noinfres  27684  ax5seg  28863  wlkoniswlk  29587  iocinioc2  32702  totprob  34405  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  36299  lshpkrlem5  39078  lshpkrlem6  39079  exatleN  39369  atbtwn  39411  atbtwnexOLDN  39412  atbtwnex  39413  4noncolr3  39418  3dimlem3a  39425  3dimlem4a  39428  3dim1  39432  3dim2  39433  1cvrat  39441  2atjlej  39444  hlatexch4  39446  ps-2b  39447  2atm  39492  2atmat  39526  4atlem11b  39573  4atlem11  39574  4at  39578  4at2  39579  2lplnja  39584  2lplnj  39585  dalemswapyz  39621  dalemccnedd  39652  cdlemb  39759  paddasslem5  39789  paddasslem15  39799  pmodlem1  39811  dalawlem1  39836  dalawlem3  39838  dalawlem4  39839  dalawlem5  39840  dalawlem6  39841  dalawlem7  39842  dalawlem8  39843  dalawlem9  39844  dalawlem11  39846  dalawlem12  39847  dalawlem15  39850  osumcllem5N  39925  osumcllem6N  39926  lhpexle3lem  39976  lhpmcvr4N  39991  lhpmcvr6N  39993  4atex2  40042  4atex2-0bOLDN  40044  4atex3  40046  ltrn11at  40112  trlval3  40152  cdlemd3  40165  cdleme0moN  40190  cdleme7aa  40207  cdleme7b  40209  cdleme7c  40210  cdleme7d  40211  cdleme7e  40212  cdleme7ga  40213  cdleme7  40214  cdleme16aN  40224  cdleme11dN  40227  cdleme11e  40228  cdleme11l  40234  cdleme11  40235  cdleme12  40236  cdleme14  40238  cdleme15b  40240  cdleme15c  40241  cdleme16b  40244  cdleme16c  40245  cdleme16d  40246  cdleme16e  40247  cdleme16f  40248  cdleme17c  40253  cdleme18c  40258  cdleme18d  40260  cdlemeda  40263  cdleme19a  40268  cdleme19b  40269  cdleme19c  40270  cdleme20aN  40274  cdleme20bN  40275  cdleme20d  40277  cdleme20i  40282  cdleme20j  40283  cdleme20l1  40285  cdleme20l2  40286  cdleme21d  40295  cdleme21e  40296  cdleme21f  40297  cdleme22aa  40304  cdleme22e  40309  cdleme22eALTN  40310  cdleme22f2  40312  cdleme22g  40313  cdleme23b  40315  cdleme26eALTN  40326  cdleme26fALTN  40327  cdleme26f  40328  cdleme26f2ALTN  40329  cdleme26f2  40330  cdleme28a  40335  cdleme28b  40336  cdleme32b  40407  cdleme32c  40408  cdleme32e  40410  cdleme35h  40421  cdleme35sn2aw  40423  cdleme41sn3aw  40439  cdleme41sn4aw  40440  cdlemeg46gfre  40497  cdlemf1  40526  cdlemg1cex  40553  cdlemg2ce  40557  cdlemg4d  40578  cdlemg4e  40579  cdlemg4f  40580  cdlemg4  40582  cdlemg6d  40586  cdlemg6e  40587  cdlemg7fvN  40589  cdlemg8b  40593  cdlemg8c  40594  cdlemg9a  40597  cdlemg9b  40598  cdlemg9  40599  cdlemg11aq  40603  cdlemg10a  40605  cdlemg12a  40608  cdlemg12b  40609  cdlemg12c  40610  cdlemg12d  40611  cdlemg13  40617  cdlemg14f  40618  cdlemg14g  40619  cdlemg17b  40627  cdlemg17dN  40628  cdlemg17e  40630  cdlemg17i  40634  cdlemg17pq  40637  cdlemg17iqN  40639  cdlemg18c  40645  cdlemg18d  40646  cdlemg18  40647  cdlemg19  40649  cdlemg21  40651  cdlemg27a  40657  cdlemg31b0N  40659  cdlemg27b  40661  cdlemg31c  40664  cdlemg33b0  40666  cdlemg33c0  40667  cdlemg33  40676  cdlemg35  40678  cdlemg43  40695  cdlemg44a  40696  cdlemg46  40700  cdlemh2  40781  cdlemh  40782  cdlemj1  40786  cdlemk3  40798  cdlemk5  40801  cdlemk6  40802  cdlemki  40806  cdlemksv2  40812  cdlemk12  40815  cdlemk15  40820  cdlemk16  40822  cdlemk18  40833  cdlemk19  40834  cdlemk7u  40835  cdlemk12u  40837  cdlemkoatnle-2N  40840  cdlemk13-2N  40841  cdlemkole-2N  40842  cdlemk14-2N  40843  cdlemk15-2N  40844  cdlemk16-2N  40845  cdlemk17-2N  40846  cdlemk18-2N  40851  cdlemk19-2N  40852  cdlemk7u-2N  40853  cdlemk11u-2N  40854  cdlemk12u-2N  40855  cdlemk20-2N  40857  cdlemk22  40858  cdlemk30  40859  cdlemk31  40861  cdlemk24-3  40868  cdlemkid2  40889  cdlemkfid3N  40890  cdlemk11ta  40894  cdlemkid3N  40898  cdlemk11tc  40910  cdlemk45  40912  cdlemk46  40913  cdlemk47  40914  cdlemk52  40919  cdlemk53a  40920  cdlemk53b  40921  cdleml1N  40941  cdleml3N  40943  cdlemn7  41168  cdlemn10  41171  dihordlem7  41179  dihord1  41183  dihord11c  41189  dihord2  41192  hlhilphllem  41924  fmuldfeq  45560  seposep  48848  iscnrm3rlem8  48869  iscnrm3llem2  48872