Theorem simp31 1228

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp131  1327  simp231  1336  simp331  1345  eqfunresadj  7366  smogt  8356  frlmphl  21961  mdetuni0  22808  mdetmul  22810  gsummatr01lem3  22844  decpmatmullem  22958  tsmsxp  24343  log2sumbnd  27739  nosupres  27902  noinfres  27917  ax5seg  29319  wlkoniswlk  30043  iocinioc2  33170  totprob  34858  cgrtr  36497  cgrtr3  36499  ofscom  36512  cgrextend  36513  segconeq  36515  ifscgr  36549  btwnxfr  36561  colinearxfr  36580  brofs2  36582  brifs2  36583  fscgr  36585  btwnconn1lem1  36592  btwnconn1lem2  36593  btwnconn1lem5  36596  btwnconn1lem6  36597  btwnconn1lem7  36598  btwnconn1lem8  36599  btwnconn1lem9  36600  btwnconn1lem10  36601  btwnconn1lem11  36602  btwnconn1lem12  36603  seglecgr12im  36615  seglecgr12  36616  segletr  36619  outsideofeq  36635  ivthALT  36879  lshpkrlem5  39921  lshpkrlem6  39922  exatleN  40211  atbtwn  40253  atbtwnexOLDN  40254  atbtwnex  40255  4noncolr3  40260  3dimlem3a  40267  3dimlem4a  40270  3dim1  40274  3dim2  40275  1cvrat  40283  2atjlej  40286  hlatexch4  40288  ps-2b  40289  2atm  40334  2atmat  40368  4atlem11b  40415  4atlem11  40416  4at  40420  4at2  40421  2lplnja  40426  2lplnj  40427  dalemswapyz  40463  dalemccnedd  40494  cdlemb  40601  paddasslem5  40631  paddasslem15  40641  pmodlem1  40653  dalawlem1  40678  dalawlem3  40680  dalawlem4  40681  dalawlem5  40682  dalawlem6  40683  dalawlem7  40684  dalawlem8  40685  dalawlem9  40686  dalawlem11  40688  dalawlem12  40689  dalawlem15  40692  osumcllem5N  40767  osumcllem6N  40768  lhpexle3lem  40818  lhpmcvr4N  40833  lhpmcvr6N  40835  4atex2  40884  4atex2-0bOLDN  40886  4atex3  40888  ltrn11at  40954  trlval3  40994  cdlemd3  41007  cdleme0moN  41032  cdleme7aa  41049  cdleme7b  41051  cdleme7c  41052  cdleme7d  41053  cdleme7e  41054  cdleme7ga  41055  cdleme7  41056  cdleme16aN  41066  cdleme11dN  41069  cdleme11e  41070  cdleme11l  41076  cdleme11  41077  cdleme12  41078  cdleme14  41080  cdleme15b  41082  cdleme15c  41083  cdleme16b  41086  cdleme16c  41087  cdleme16d  41088  cdleme16e  41089  cdleme16f  41090  cdleme17c  41095  cdleme18c  41100  cdleme18d  41102  cdlemeda  41105  cdleme19a  41110  cdleme19b  41111  cdleme19c  41112  cdleme20aN  41116  cdleme20bN  41117  cdleme20d  41119  cdleme20i  41124  cdleme20j  41125  cdleme20l1  41127  cdleme20l2  41128  cdleme21d  41137  cdleme21e  41138  cdleme21f  41139  cdleme22aa  41146  cdleme22e  41151  cdleme22eALTN  41152  cdleme22f2  41154  cdleme22g  41155  cdleme23b  41157  cdleme26eALTN  41168  cdleme26fALTN  41169  cdleme26f  41170  cdleme26f2ALTN  41171  cdleme26f2  41172  cdleme28a  41177  cdleme28b  41178  cdleme32b  41249  cdleme32c  41250  cdleme32e  41252  cdleme35h  41263  cdleme35sn2aw  41265  cdleme41sn3aw  41281  cdleme41sn4aw  41282  cdlemeg46gfre  41339  cdlemf1  41368  cdlemg1cex  41395  cdlemg2ce  41399  cdlemg4d  41420  cdlemg4e  41421  cdlemg4f  41422  cdlemg4  41424  cdlemg6d  41428  cdlemg6e  41429  cdlemg7fvN  41431  cdlemg8b  41435  cdlemg8c  41436  cdlemg9a  41439  cdlemg9b  41440  cdlemg9  41441  cdlemg11aq  41445  cdlemg10a  41447  cdlemg12a  41450  cdlemg12b  41451  cdlemg12c  41452  cdlemg12d  41453  cdlemg13  41459  cdlemg14f  41460  cdlemg14g  41461  cdlemg17b  41469  cdlemg17dN  41470  cdlemg17e  41472  cdlemg17i  41476  cdlemg17pq  41479  cdlemg17iqN  41481  cdlemg18c  41487  cdlemg18d  41488  cdlemg18  41489  cdlemg19  41491  cdlemg21  41493  cdlemg27a  41499  cdlemg31b0N  41501  cdlemg27b  41503  cdlemg31c  41506  cdlemg33b0  41508  cdlemg33c0  41509  cdlemg33  41518  cdlemg35  41520  cdlemg43  41537  cdlemg44a  41538  cdlemg46  41542  cdlemh2  41623  cdlemh  41624  cdlemj1  41628  cdlemk3  41640  cdlemk5  41643  cdlemk6  41644  cdlemki  41648  cdlemksv2  41654  cdlemk12  41657  cdlemk15  41662  cdlemk16  41664  cdlemk18  41675  cdlemk19  41676  cdlemk7u  41677  cdlemk12u  41679  cdlemkoatnle-2N  41682  cdlemk13-2N  41683  cdlemkole-2N  41684  cdlemk14-2N  41685  cdlemk15-2N  41686  cdlemk16-2N  41687  cdlemk17-2N  41688  cdlemk18-2N  41693  cdlemk19-2N  41694  cdlemk7u-2N  41695  cdlemk11u-2N  41696  cdlemk12u-2N  41697  cdlemk20-2N  41699  cdlemk22  41700  cdlemk30  41701  cdlemk31  41703  cdlemk24-3  41710  cdlemkid2  41731  cdlemkfid3N  41732  cdlemk11ta  41736  cdlemkid3N  41740  cdlemk11tc  41752  cdlemk45  41754  cdlemk46  41755  cdlemk47  41756  cdlemk52  41761  cdlemk53a  41762  cdlemk53b  41763  cdleml1N  41783  cdleml3N  41785  cdlemn7  42010  cdlemn10  42013  dihordlem7  42021  dihord1  42025  dihord11c  42031  dihord2  42034  hlhilphllem  42766  fmuldfeq  46332  seposep  49737  iscnrm3rlem8  49758  iscnrm3llem2  49761