Theorem simp31 1202

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

Syntax hints:   → wi 4   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  simp131  1301  simp231  1310  simp331  1319  smogt  7856  frlmphl  20607  mdetuni0  20914  mdetmul  20916  gsummatr01lem3  20950  decpmatmullem  21063  tsmsxp  22446  log2sumbnd  25802  ax5seg  26407  wlkoniswlk  27125  iocinioc2  30190  totprob  31302  eqfunresadj  32612  nosupres  32816  cgrtr  33062  cgrtr3  33064  ofscom  33077  cgrextend  33078  segconeq  33080  ifscgr  33114  btwnxfr  33126  colinearxfr  33145  brofs2  33147  brifs2  33148  fscgr  33150  btwnconn1lem1  33157  btwnconn1lem2  33158  btwnconn1lem5  33161  btwnconn1lem6  33162  btwnconn1lem7  33163  btwnconn1lem8  33164  btwnconn1lem9  33165  btwnconn1lem10  33166  btwnconn1lem11  33167  btwnconn1lem12  33168  seglecgr12im  33180  seglecgr12  33181  segletr  33184  outsideofeq  33200  ivthALT  33292  lshpkrlem5  35781  lshpkrlem6  35782  exatleN  36071  atbtwn  36113  atbtwnexOLDN  36114  atbtwnex  36115  4noncolr3  36120  3dimlem3a  36127  3dimlem4a  36130  3dim1  36134  3dim2  36135  1cvrat  36143  2atjlej  36146  hlatexch4  36148  ps-2b  36149  2atm  36194  2atmat  36228  4atlem11b  36275  4atlem11  36276  4at  36280  4at2  36281  2lplnja  36286  2lplnj  36287  dalemswapyz  36323  dalemccnedd  36354  cdlemb  36461  paddasslem5  36491  paddasslem15  36501  pmodlem1  36513  dalawlem1  36538  dalawlem3  36540  dalawlem4  36541  dalawlem5  36542  dalawlem6  36543  dalawlem7  36544  dalawlem8  36545  dalawlem9  36546  dalawlem11  36548  dalawlem12  36549  dalawlem15  36552  osumcllem5N  36627  osumcllem6N  36628  lhpexle3lem  36678  lhpmcvr4N  36693  lhpmcvr6N  36695  4atex2  36744  4atex2-0bOLDN  36746  4atex3  36748  ltrn11at  36814  trlval3  36854  cdlemd3  36867  cdleme0moN  36892  cdleme7aa  36909  cdleme7b  36911  cdleme7c  36912  cdleme7d  36913  cdleme7e  36914  cdleme7ga  36915  cdleme7  36916  cdleme16aN  36926  cdleme11dN  36929  cdleme11e  36930  cdleme11l  36936  cdleme11  36937  cdleme12  36938  cdleme14  36940  cdleme15b  36942  cdleme15c  36943  cdleme16b  36946  cdleme16c  36947  cdleme16d  36948  cdleme16e  36949  cdleme16f  36950  cdleme17c  36955  cdleme18c  36960  cdleme18d  36962  cdlemeda  36965  cdleme19a  36970  cdleme19b  36971  cdleme19c  36972  cdleme20aN  36976  cdleme20bN  36977  cdleme20d  36979  cdleme20i  36984  cdleme20j  36985  cdleme20l1  36987  cdleme20l2  36988  cdleme21d  36997  cdleme21e  36998  cdleme21f  36999  cdleme22aa  37006  cdleme22e  37011  cdleme22eALTN  37012  cdleme22f2  37014  cdleme22g  37015  cdleme23b  37017  cdleme26eALTN  37028  cdleme26fALTN  37029  cdleme26f  37030  cdleme26f2ALTN  37031  cdleme26f2  37032  cdleme28a  37037  cdleme28b  37038  cdleme32b  37109  cdleme32c  37110  cdleme32e  37112  cdleme35h  37123  cdleme35sn2aw  37125  cdleme41sn3aw  37141  cdleme41sn4aw  37142  cdlemeg46gfre  37199  cdlemf1  37228  cdlemg1cex  37255  cdlemg2ce  37259  cdlemg4d  37280  cdlemg4e  37281  cdlemg4f  37282  cdlemg4  37284  cdlemg6d  37288  cdlemg6e  37289  cdlemg7fvN  37291  cdlemg8b  37295  cdlemg8c  37296  cdlemg9a  37299  cdlemg9b  37300  cdlemg9  37301  cdlemg11aq  37305  cdlemg10a  37307  cdlemg12a  37310  cdlemg12b  37311  cdlemg12c  37312  cdlemg12d  37313  cdlemg13  37319  cdlemg14f  37320  cdlemg14g  37321  cdlemg17b  37329  cdlemg17dN  37330  cdlemg17e  37332  cdlemg17i  37336  cdlemg17pq  37339  cdlemg17iqN  37341  cdlemg18c  37347  cdlemg18d  37348  cdlemg18  37349  cdlemg19  37351  cdlemg21  37353  cdlemg27a  37359  cdlemg31b0N  37361  cdlemg27b  37363  cdlemg31c  37366  cdlemg33b0  37368  cdlemg33c0  37369  cdlemg33  37378  cdlemg35  37380  cdlemg43  37397  cdlemg44a  37398  cdlemg46  37402  cdlemh2  37483  cdlemh  37484  cdlemj1  37488  cdlemk3  37500  cdlemk5  37503  cdlemk6  37504  cdlemki  37508  cdlemksv2  37514  cdlemk12  37517  cdlemk15  37522  cdlemk16  37524  cdlemk18  37535  cdlemk19  37536  cdlemk7u  37537  cdlemk12u  37539  cdlemkoatnle-2N  37542  cdlemk13-2N  37543  cdlemkole-2N  37544  cdlemk14-2N  37545  cdlemk15-2N  37546  cdlemk16-2N  37547  cdlemk17-2N  37548  cdlemk18-2N  37553  cdlemk19-2N  37554  cdlemk7u-2N  37555  cdlemk11u-2N  37556  cdlemk12u-2N  37557  cdlemk20-2N  37559  cdlemk22  37560  cdlemk30  37561  cdlemk31  37563  cdlemk24-3  37570  cdlemkid2  37591  cdlemkfid3N  37592  cdlemk11ta  37596  cdlemkid3N  37600  cdlemk11tc  37612  cdlemk45  37614  cdlemk46  37615  cdlemk47  37616  cdlemk52  37621  cdlemk53a  37622  cdlemk53b  37623  cdleml1N  37643  cdleml3N  37645  cdlemn7  37870  cdlemn10  37873  dihordlem7  37881  dihord1  37885  dihord11c  37891  dihord2  37894  hlhilphllem  38626  fmuldfeq  41406