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  7306  smogt  8299  frlmphl  21736  mdetuni0  22565  mdetmul  22567  gsummatr01lem3  22601  decpmatmullem  22715  tsmsxp  24099  log2sumbnd  27511  nosupres  27675  noinfres  27690  ax5seg  29011  wlkoniswlk  29733  iocinioc2  32859  totprob  34584  cgrtr  36186  cgrtr3  36188  ofscom  36201  cgrextend  36202  segconeq  36204  ifscgr  36238  btwnxfr  36250  colinearxfr  36269  brofs2  36271  brifs2  36272  fscgr  36274  btwnconn1lem1  36281  btwnconn1lem2  36282  btwnconn1lem5  36285  btwnconn1lem6  36286  btwnconn1lem7  36287  btwnconn1lem8  36288  btwnconn1lem9  36289  btwnconn1lem10  36290  btwnconn1lem11  36291  btwnconn1lem12  36292  seglecgr12im  36304  seglecgr12  36305  segletr  36308  outsideofeq  36324  ivthALT  36529  lshpkrlem5  39374  lshpkrlem6  39375  exatleN  39664  atbtwn  39706  atbtwnexOLDN  39707  atbtwnex  39708  4noncolr3  39713  3dimlem3a  39720  3dimlem4a  39723  3dim1  39727  3dim2  39728  1cvrat  39736  2atjlej  39739  hlatexch4  39741  ps-2b  39742  2atm  39787  2atmat  39821  4atlem11b  39868  4atlem11  39869  4at  39873  4at2  39874  2lplnja  39879  2lplnj  39880  dalemswapyz  39916  dalemccnedd  39947  cdlemb  40054  paddasslem5  40084  paddasslem15  40094  pmodlem1  40106  dalawlem1  40131  dalawlem3  40133  dalawlem4  40134  dalawlem5  40135  dalawlem6  40136  dalawlem7  40137  dalawlem8  40138  dalawlem9  40139  dalawlem11  40141  dalawlem12  40142  dalawlem15  40145  osumcllem5N  40220  osumcllem6N  40221  lhpexle3lem  40271  lhpmcvr4N  40286  lhpmcvr6N  40288  4atex2  40337  4atex2-0bOLDN  40339  4atex3  40341  ltrn11at  40407  trlval3  40447  cdlemd3  40460  cdleme0moN  40485  cdleme7aa  40502  cdleme7b  40504  cdleme7c  40505  cdleme7d  40506  cdleme7e  40507  cdleme7ga  40508  cdleme7  40509  cdleme16aN  40519  cdleme11dN  40522  cdleme11e  40523  cdleme11l  40529  cdleme11  40530  cdleme12  40531  cdleme14  40533  cdleme15b  40535  cdleme15c  40536  cdleme16b  40539  cdleme16c  40540  cdleme16d  40541  cdleme16e  40542  cdleme16f  40543  cdleme17c  40548  cdleme18c  40553  cdleme18d  40555  cdlemeda  40558  cdleme19a  40563  cdleme19b  40564  cdleme19c  40565  cdleme20aN  40569  cdleme20bN  40570  cdleme20d  40572  cdleme20i  40577  cdleme20j  40578  cdleme20l1  40580  cdleme20l2  40581  cdleme21d  40590  cdleme21e  40591  cdleme21f  40592  cdleme22aa  40599  cdleme22e  40604  cdleme22eALTN  40605  cdleme22f2  40607  cdleme22g  40608  cdleme23b  40610  cdleme26eALTN  40621  cdleme26fALTN  40622  cdleme26f  40623  cdleme26f2ALTN  40624  cdleme26f2  40625  cdleme28a  40630  cdleme28b  40631  cdleme32b  40702  cdleme32c  40703  cdleme32e  40705  cdleme35h  40716  cdleme35sn2aw  40718  cdleme41sn3aw  40734  cdleme41sn4aw  40735  cdlemeg46gfre  40792  cdlemf1  40821  cdlemg1cex  40848  cdlemg2ce  40852  cdlemg4d  40873  cdlemg4e  40874  cdlemg4f  40875  cdlemg4  40877  cdlemg6d  40881  cdlemg6e  40882  cdlemg7fvN  40884  cdlemg8b  40888  cdlemg8c  40889  cdlemg9a  40892  cdlemg9b  40893  cdlemg9  40894  cdlemg11aq  40898  cdlemg10a  40900  cdlemg12a  40903  cdlemg12b  40904  cdlemg12c  40905  cdlemg12d  40906  cdlemg13  40912  cdlemg14f  40913  cdlemg14g  40914  cdlemg17b  40922  cdlemg17dN  40923  cdlemg17e  40925  cdlemg17i  40929  cdlemg17pq  40932  cdlemg17iqN  40934  cdlemg18c  40940  cdlemg18d  40941  cdlemg18  40942  cdlemg19  40944  cdlemg21  40946  cdlemg27a  40952  cdlemg31b0N  40954  cdlemg27b  40956  cdlemg31c  40959  cdlemg33b0  40961  cdlemg33c0  40962  cdlemg33  40971  cdlemg35  40973  cdlemg43  40990  cdlemg44a  40991  cdlemg46  40995  cdlemh2  41076  cdlemh  41077  cdlemj1  41081  cdlemk3  41093  cdlemk5  41096  cdlemk6  41097  cdlemki  41101  cdlemksv2  41107  cdlemk12  41110  cdlemk15  41115  cdlemk16  41117  cdlemk18  41128  cdlemk19  41129  cdlemk7u  41130  cdlemk12u  41132  cdlemkoatnle-2N  41135  cdlemk13-2N  41136  cdlemkole-2N  41137  cdlemk14-2N  41138  cdlemk15-2N  41139  cdlemk16-2N  41140  cdlemk17-2N  41141  cdlemk18-2N  41146  cdlemk19-2N  41147  cdlemk7u-2N  41148  cdlemk11u-2N  41149  cdlemk12u-2N  41150  cdlemk20-2N  41152  cdlemk22  41153  cdlemk30  41154  cdlemk31  41156  cdlemk24-3  41163  cdlemkid2  41184  cdlemkfid3N  41185  cdlemk11ta  41189  cdlemkid3N  41193  cdlemk11tc  41205  cdlemk45  41207  cdlemk46  41208  cdlemk47  41209  cdlemk52  41214  cdlemk53a  41215  cdlemk53b  41216  cdleml1N  41236  cdleml3N  41238  cdlemn7  41463  cdlemn10  41466  dihordlem7  41474  dihord1  41478  dihord11c  41484  dihord2  41487  hlhilphllem  42219  fmuldfeq  45829  seposep  49171  iscnrm3rlem8  49192  iscnrm3llem2  49195