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  7338  smogt  8339  frlmphl  21697  mdetuni0  22515  mdetmul  22517  gsummatr01lem3  22551  decpmatmullem  22665  tsmsxp  24049  log2sumbnd  27462  nosupres  27626  noinfres  27641  ax5seg  28872  wlkoniswlk  29596  iocinioc2  32709  totprob  34425  cgrtr  35987  cgrtr3  35989  ofscom  36002  cgrextend  36003  segconeq  36005  ifscgr  36039  btwnxfr  36051  colinearxfr  36070  brofs2  36072  brifs2  36073  fscgr  36075  btwnconn1lem1  36082  btwnconn1lem2  36083  btwnconn1lem5  36086  btwnconn1lem6  36087  btwnconn1lem7  36088  btwnconn1lem8  36089  btwnconn1lem9  36090  btwnconn1lem10  36091  btwnconn1lem11  36092  btwnconn1lem12  36093  seglecgr12im  36105  seglecgr12  36106  segletr  36109  outsideofeq  36125  ivthALT  36330  lshpkrlem5  39114  lshpkrlem6  39115  exatleN  39405  atbtwn  39447  atbtwnexOLDN  39448  atbtwnex  39449  4noncolr3  39454  3dimlem3a  39461  3dimlem4a  39464  3dim1  39468  3dim2  39469  1cvrat  39477  2atjlej  39480  hlatexch4  39482  ps-2b  39483  2atm  39528  2atmat  39562  4atlem11b  39609  4atlem11  39610  4at  39614  4at2  39615  2lplnja  39620  2lplnj  39621  dalemswapyz  39657  dalemccnedd  39688  cdlemb  39795  paddasslem5  39825  paddasslem15  39835  pmodlem1  39847  dalawlem1  39872  dalawlem3  39874  dalawlem4  39875  dalawlem5  39876  dalawlem6  39877  dalawlem7  39878  dalawlem8  39879  dalawlem9  39880  dalawlem11  39882  dalawlem12  39883  dalawlem15  39886  osumcllem5N  39961  osumcllem6N  39962  lhpexle3lem  40012  lhpmcvr4N  40027  lhpmcvr6N  40029  4atex2  40078  4atex2-0bOLDN  40080  4atex3  40082  ltrn11at  40148  trlval3  40188  cdlemd3  40201  cdleme0moN  40226  cdleme7aa  40243  cdleme7b  40245  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme7  40250  cdleme16aN  40260  cdleme11dN  40263  cdleme11e  40264  cdleme11l  40270  cdleme11  40271  cdleme12  40272  cdleme14  40274  cdleme15b  40276  cdleme15c  40277  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme16e  40283  cdleme16f  40284  cdleme17c  40289  cdleme18c  40294  cdleme18d  40296  cdlemeda  40299  cdleme19a  40304  cdleme19b  40305  cdleme19c  40306  cdleme20aN  40310  cdleme20bN  40311  cdleme20d  40313  cdleme20i  40318  cdleme20j  40319  cdleme20l1  40321  cdleme20l2  40322  cdleme21d  40331  cdleme21e  40332  cdleme21f  40333  cdleme22aa  40340  cdleme22e  40345  cdleme22eALTN  40346  cdleme22f2  40348  cdleme22g  40349  cdleme23b  40351  cdleme26eALTN  40362  cdleme26fALTN  40363  cdleme26f  40364  cdleme26f2ALTN  40365  cdleme26f2  40366  cdleme28a  40371  cdleme28b  40372  cdleme32b  40443  cdleme32c  40444  cdleme32e  40446  cdleme35h  40457  cdleme35sn2aw  40459  cdleme41sn3aw  40475  cdleme41sn4aw  40476  cdlemeg46gfre  40533  cdlemf1  40562  cdlemg1cex  40589  cdlemg2ce  40593  cdlemg4d  40614  cdlemg4e  40615  cdlemg4f  40616  cdlemg4  40618  cdlemg6d  40622  cdlemg6e  40623  cdlemg7fvN  40625  cdlemg8b  40629  cdlemg8c  40630  cdlemg9a  40633  cdlemg9b  40634  cdlemg9  40635  cdlemg11aq  40639  cdlemg10a  40641  cdlemg12a  40644  cdlemg12b  40645  cdlemg12c  40646  cdlemg12d  40647  cdlemg13  40653  cdlemg14f  40654  cdlemg14g  40655  cdlemg17b  40663  cdlemg17dN  40664  cdlemg17e  40666  cdlemg17i  40670  cdlemg17pq  40673  cdlemg17iqN  40675  cdlemg18c  40681  cdlemg18d  40682  cdlemg18  40683  cdlemg19  40685  cdlemg21  40687  cdlemg27a  40693  cdlemg31b0N  40695  cdlemg27b  40697  cdlemg31c  40700  cdlemg33b0  40702  cdlemg33c0  40703  cdlemg33  40712  cdlemg35  40714  cdlemg43  40731  cdlemg44a  40732  cdlemg46  40736  cdlemh2  40817  cdlemh  40818  cdlemj1  40822  cdlemk3  40834  cdlemk5  40837  cdlemk6  40838  cdlemki  40842  cdlemksv2  40848  cdlemk12  40851  cdlemk15  40856  cdlemk16  40858  cdlemk18  40869  cdlemk19  40870  cdlemk7u  40871  cdlemk12u  40873  cdlemkoatnle-2N  40876  cdlemk13-2N  40877  cdlemkole-2N  40878  cdlemk14-2N  40879  cdlemk15-2N  40880  cdlemk16-2N  40881  cdlemk17-2N  40882  cdlemk18-2N  40887  cdlemk19-2N  40888  cdlemk7u-2N  40889  cdlemk11u-2N  40890  cdlemk12u-2N  40891  cdlemk20-2N  40893  cdlemk22  40894  cdlemk30  40895  cdlemk31  40897  cdlemk24-3  40904  cdlemkid2  40925  cdlemkfid3N  40926  cdlemk11ta  40930  cdlemkid3N  40934  cdlemk11tc  40946  cdlemk45  40948  cdlemk46  40949  cdlemk47  40950  cdlemk52  40955  cdlemk53a  40956  cdlemk53b  40957  cdleml1N  40977  cdleml3N  40979  cdlemn7  41204  cdlemn10  41207  dihordlem7  41215  dihord1  41219  dihord11c  41225  dihord2  41228  hlhilphllem  41960  fmuldfeq  45588  seposep  48918  iscnrm3rlem8  48939  iscnrm3llem2  48942