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  7317  smogt  8313  frlmphl  21666  mdetuni0  22484  mdetmul  22486  gsummatr01lem3  22520  decpmatmullem  22634  tsmsxp  24018  log2sumbnd  27431  nosupres  27595  noinfres  27610  ax5seg  28841  wlkoniswlk  29563  iocinioc2  32675  totprob  34391  cgrtr  35953  cgrtr3  35955  ofscom  35968  cgrextend  35969  segconeq  35971  ifscgr  36005  btwnxfr  36017  colinearxfr  36036  brofs2  36038  brifs2  36039  fscgr  36041  btwnconn1lem1  36048  btwnconn1lem2  36049  btwnconn1lem5  36052  btwnconn1lem6  36053  btwnconn1lem7  36054  btwnconn1lem8  36055  btwnconn1lem9  36056  btwnconn1lem10  36057  btwnconn1lem11  36058  btwnconn1lem12  36059  seglecgr12im  36071  seglecgr12  36072  segletr  36075  outsideofeq  36091  ivthALT  36296  lshpkrlem5  39080  lshpkrlem6  39081  exatleN  39371  atbtwn  39413  atbtwnexOLDN  39414  atbtwnex  39415  4noncolr3  39420  3dimlem3a  39427  3dimlem4a  39430  3dim1  39434  3dim2  39435  1cvrat  39443  2atjlej  39446  hlatexch4  39448  ps-2b  39449  2atm  39494  2atmat  39528  4atlem11b  39575  4atlem11  39576  4at  39580  4at2  39581  2lplnja  39586  2lplnj  39587  dalemswapyz  39623  dalemccnedd  39654  cdlemb  39761  paddasslem5  39791  paddasslem15  39801  pmodlem1  39813  dalawlem1  39838  dalawlem3  39840  dalawlem4  39841  dalawlem5  39842  dalawlem6  39843  dalawlem7  39844  dalawlem8  39845  dalawlem9  39846  dalawlem11  39848  dalawlem12  39849  dalawlem15  39852  osumcllem5N  39927  osumcllem6N  39928  lhpexle3lem  39978  lhpmcvr4N  39993  lhpmcvr6N  39995  4atex2  40044  4atex2-0bOLDN  40046  4atex3  40048  ltrn11at  40114  trlval3  40154  cdlemd3  40167  cdleme0moN  40192  cdleme7aa  40209  cdleme7b  40211  cdleme7c  40212  cdleme7d  40213  cdleme7e  40214  cdleme7ga  40215  cdleme7  40216  cdleme16aN  40226  cdleme11dN  40229  cdleme11e  40230  cdleme11l  40236  cdleme11  40237  cdleme12  40238  cdleme14  40240  cdleme15b  40242  cdleme15c  40243  cdleme16b  40246  cdleme16c  40247  cdleme16d  40248  cdleme16e  40249  cdleme16f  40250  cdleme17c  40255  cdleme18c  40260  cdleme18d  40262  cdlemeda  40265  cdleme19a  40270  cdleme19b  40271  cdleme19c  40272  cdleme20aN  40276  cdleme20bN  40277  cdleme20d  40279  cdleme20i  40284  cdleme20j  40285  cdleme20l1  40287  cdleme20l2  40288  cdleme21d  40297  cdleme21e  40298  cdleme21f  40299  cdleme22aa  40306  cdleme22e  40311  cdleme22eALTN  40312  cdleme22f2  40314  cdleme22g  40315  cdleme23b  40317  cdleme26eALTN  40328  cdleme26fALTN  40329  cdleme26f  40330  cdleme26f2ALTN  40331  cdleme26f2  40332  cdleme28a  40337  cdleme28b  40338  cdleme32b  40409  cdleme32c  40410  cdleme32e  40412  cdleme35h  40423  cdleme35sn2aw  40425  cdleme41sn3aw  40441  cdleme41sn4aw  40442  cdlemeg46gfre  40499  cdlemf1  40528  cdlemg1cex  40555  cdlemg2ce  40559  cdlemg4d  40580  cdlemg4e  40581  cdlemg4f  40582  cdlemg4  40584  cdlemg6d  40588  cdlemg6e  40589  cdlemg7fvN  40591  cdlemg8b  40595  cdlemg8c  40596  cdlemg9a  40599  cdlemg9b  40600  cdlemg9  40601  cdlemg11aq  40605  cdlemg10a  40607  cdlemg12a  40610  cdlemg12b  40611  cdlemg12c  40612  cdlemg12d  40613  cdlemg13  40619  cdlemg14f  40620  cdlemg14g  40621  cdlemg17b  40629  cdlemg17dN  40630  cdlemg17e  40632  cdlemg17i  40636  cdlemg17pq  40639  cdlemg17iqN  40641  cdlemg18c  40647  cdlemg18d  40648  cdlemg18  40649  cdlemg19  40651  cdlemg21  40653  cdlemg27a  40659  cdlemg31b0N  40661  cdlemg27b  40663  cdlemg31c  40666  cdlemg33b0  40668  cdlemg33c0  40669  cdlemg33  40678  cdlemg35  40680  cdlemg43  40697  cdlemg44a  40698  cdlemg46  40702  cdlemh2  40783  cdlemh  40784  cdlemj1  40788  cdlemk3  40800  cdlemk5  40803  cdlemk6  40804  cdlemki  40808  cdlemksv2  40814  cdlemk12  40817  cdlemk15  40822  cdlemk16  40824  cdlemk18  40835  cdlemk19  40836  cdlemk7u  40837  cdlemk12u  40839  cdlemkoatnle-2N  40842  cdlemk13-2N  40843  cdlemkole-2N  40844  cdlemk14-2N  40845  cdlemk15-2N  40846  cdlemk16-2N  40847  cdlemk17-2N  40848  cdlemk18-2N  40853  cdlemk19-2N  40854  cdlemk7u-2N  40855  cdlemk11u-2N  40856  cdlemk12u-2N  40857  cdlemk20-2N  40859  cdlemk22  40860  cdlemk30  40861  cdlemk31  40863  cdlemk24-3  40870  cdlemkid2  40891  cdlemkfid3N  40892  cdlemk11ta  40896  cdlemkid3N  40900  cdlemk11tc  40912  cdlemk45  40914  cdlemk46  40915  cdlemk47  40916  cdlemk52  40921  cdlemk53a  40922  cdlemk53b  40923  cdleml1N  40943  cdleml3N  40945  cdlemn7  41170  cdlemn10  41173  dihordlem7  41181  dihord1  41185  dihord11c  41191  dihord2  41194  hlhilphllem  41926  fmuldfeq  45554  seposep  48887  iscnrm3rlem8  48908  iscnrm3llem2  48911