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  7301  smogt  8297  frlmphl  21707  mdetuni0  22525  mdetmul  22527  gsummatr01lem3  22561  decpmatmullem  22675  tsmsxp  24059  log2sumbnd  27472  nosupres  27636  noinfres  27651  ax5seg  28902  wlkoniswlk  29624  iocinioc2  32741  totprob  34414  cgrtr  35985  cgrtr3  35987  ofscom  36000  cgrextend  36001  segconeq  36003  ifscgr  36037  btwnxfr  36049  colinearxfr  36068  brofs2  36070  brifs2  36071  fscgr  36073  btwnconn1lem1  36080  btwnconn1lem2  36081  btwnconn1lem5  36084  btwnconn1lem6  36085  btwnconn1lem7  36086  btwnconn1lem8  36087  btwnconn1lem9  36088  btwnconn1lem10  36089  btwnconn1lem11  36090  btwnconn1lem12  36091  seglecgr12im  36103  seglecgr12  36104  segletr  36107  outsideofeq  36123  ivthALT  36328  lshpkrlem5  39112  lshpkrlem6  39113  exatleN  39403  atbtwn  39445  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  2atmat  39560  4atlem11b  39607  4atlem11  39608  4at  39612  4at2  39613  2lplnja  39618  2lplnj  39619  dalemswapyz  39655  dalemccnedd  39686  cdlemb  39793  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  4atex2  40076  4atex2-0bOLDN  40078  4atex3  40080  ltrn11at  40146  trlval3  40186  cdlemd3  40199  cdleme0moN  40224  cdleme7aa  40241  cdleme7b  40243  cdleme7c  40244  cdleme7d  40245  cdleme7e  40246  cdleme7ga  40247  cdleme7  40248  cdleme16aN  40258  cdleme11dN  40261  cdleme11e  40262  cdleme11l  40268  cdleme11  40269  cdleme12  40270  cdleme14  40272  cdleme15b  40274  cdleme15c  40275  cdleme16b  40278  cdleme16c  40279  cdleme16d  40280  cdleme16e  40281  cdleme16f  40282  cdleme17c  40287  cdleme18c  40292  cdleme18d  40294  cdlemeda  40297  cdleme19a  40302  cdleme19b  40303  cdleme19c  40304  cdleme20aN  40308  cdleme20bN  40309  cdleme20d  40311  cdleme20i  40316  cdleme20j  40317  cdleme20l1  40319  cdleme20l2  40320  cdleme21d  40329  cdleme21e  40330  cdleme21f  40331  cdleme22aa  40338  cdleme22e  40343  cdleme22eALTN  40344  cdleme22f2  40346  cdleme22g  40347  cdleme23b  40349  cdleme26eALTN  40360  cdleme26fALTN  40361  cdleme26f  40362  cdleme26f2ALTN  40363  cdleme26f2  40364  cdleme28a  40369  cdleme28b  40370  cdleme32b  40441  cdleme32c  40442  cdleme32e  40444  cdleme35h  40455  cdleme35sn2aw  40457  cdleme41sn3aw  40473  cdleme41sn4aw  40474  cdlemeg46gfre  40531  cdlemf1  40560  cdlemg1cex  40587  cdlemg2ce  40591  cdlemg4d  40612  cdlemg4e  40613  cdlemg4f  40614  cdlemg4  40616  cdlemg6d  40620  cdlemg6e  40621  cdlemg7fvN  40623  cdlemg8b  40627  cdlemg8c  40628  cdlemg9a  40631  cdlemg9b  40632  cdlemg9  40633  cdlemg11aq  40637  cdlemg10a  40639  cdlemg12a  40642  cdlemg12b  40643  cdlemg12c  40644  cdlemg12d  40645  cdlemg13  40651  cdlemg14f  40652  cdlemg14g  40653  cdlemg17b  40661  cdlemg17dN  40662  cdlemg17e  40664  cdlemg17i  40668  cdlemg17pq  40671  cdlemg17iqN  40673  cdlemg18c  40679  cdlemg18d  40680  cdlemg18  40681  cdlemg19  40683  cdlemg21  40685  cdlemg27a  40691  cdlemg31b0N  40693  cdlemg27b  40695  cdlemg31c  40698  cdlemg33b0  40700  cdlemg33c0  40701  cdlemg33  40710  cdlemg35  40712  cdlemg43  40729  cdlemg44a  40730  cdlemg46  40734  cdlemh2  40815  cdlemh  40816  cdlemj1  40820  cdlemk3  40832  cdlemk5  40835  cdlemk6  40836  cdlemki  40840  cdlemksv2  40846  cdlemk12  40849  cdlemk15  40854  cdlemk16  40856  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  cdlemk20-2N  40891  cdlemk22  40892  cdlemk30  40893  cdlemk31  40895  cdlemk24-3  40902  cdlemkid2  40923  cdlemkfid3N  40924  cdlemk11ta  40928  cdlemkid3N  40932  cdlemk11tc  40944  cdlemk45  40946  cdlemk46  40947  cdlemk47  40948  cdlemk52  40953  cdlemk53a  40954  cdlemk53b  40955  cdleml1N  40975  cdleml3N  40977  cdlemn7  41202  cdlemn10  41205  dihordlem7  41213  dihord1  41217  dihord11c  41223  dihord2  41226  hlhilphllem  41958  fmuldfeq  45584  seposep  48930  iscnrm3rlem8  48951  iscnrm3llem2  48954