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  7374  smogt  8382  frlmphl  22096  mdetuni0  22945  mdetmul  22947  gsummatr01lem3  22981  decpmatmullem  23098  tsmsxp  24483  log2sumbnd  27880  nosupres  28073  noinfres  28088  ax5seg  29525  wlkoniswlk  30249  iocinioc2  33421  totprob  35109  cgrtr  36853  cgrtr3  36855  ofscom  36868  cgrextend  36869  segconeq  36871  ifscgr  36905  btwnxfr  36917  colinearxfr  36936  brofs2  36938  brifs2  36939  fscgr  36941  btwnconn1lem1  36948  btwnconn1lem2  36949  btwnconn1lem5  36952  btwnconn1lem6  36953  btwnconn1lem7  36954  btwnconn1lem8  36955  btwnconn1lem9  36956  btwnconn1lem10  36957  btwnconn1lem11  36958  btwnconn1lem12  36959  seglecgr12im  36971  seglecgr12  36972  segletr  36975  outsideofeq  36991  ivthALT  37219  lshpkrlem5  40280  lshpkrlem6  40281  exatleN  40570  atbtwn  40612  atbtwnexOLDN  40613  atbtwnex  40614  4noncolr3  40619  3dimlem3a  40626  3dimlem4a  40629  3dim1  40633  3dim2  40634  1cvrat  40642  2atjlej  40645  hlatexch4  40647  ps-2b  40648  2atm  40693  2atmat  40727  4atlem11b  40774  4atlem11  40775  4at  40779  4at2  40780  2lplnja  40785  2lplnj  40786  dalemswapyz  40822  dalemccnedd  40853  cdlemb  40960  paddasslem5  40990  paddasslem15  41000  pmodlem1  41012  dalawlem1  41037  dalawlem3  41039  dalawlem4  41040  dalawlem5  41041  dalawlem6  41042  dalawlem7  41043  dalawlem8  41044  dalawlem9  41045  dalawlem11  41047  dalawlem12  41048  dalawlem15  41051  osumcllem5N  41126  osumcllem6N  41127  lhpexle3lem  41177  lhpmcvr4N  41192  lhpmcvr6N  41194  4atex2  41243  4atex2-0bOLDN  41245  4atex3  41247  ltrn11at  41313  trlval3  41353  cdlemd3  41366  cdleme0moN  41391  cdleme7aa  41408  cdleme7b  41410  cdleme7c  41411  cdleme7d  41412  cdleme7e  41413  cdleme7ga  41414  cdleme7  41415  cdleme16aN  41425  cdleme11dN  41428  cdleme11e  41429  cdleme11l  41435  cdleme11  41436  cdleme12  41437  cdleme14  41439  cdleme15b  41441  cdleme15c  41442  cdleme16b  41445  cdleme16c  41446  cdleme16d  41447  cdleme16e  41448  cdleme16f  41449  cdleme17c  41454  cdleme18c  41459  cdleme18d  41461  cdlemeda  41464  cdleme19a  41469  cdleme19b  41470  cdleme19c  41471  cdleme20aN  41475  cdleme20bN  41476  cdleme20d  41478  cdleme20i  41483  cdleme20j  41484  cdleme20l1  41486  cdleme20l2  41487  cdleme21d  41496  cdleme21e  41497  cdleme21f  41498  cdleme22aa  41505  cdleme22e  41510  cdleme22eALTN  41511  cdleme22f2  41513  cdleme22g  41514  cdleme23b  41516  cdleme26eALTN  41527  cdleme26fALTN  41528  cdleme26f  41529  cdleme26f2ALTN  41530  cdleme26f2  41531  cdleme28a  41536  cdleme28b  41537  cdleme32b  41608  cdleme32c  41609  cdleme32e  41611  cdleme35h  41622  cdleme35sn2aw  41624  cdleme41sn3aw  41640  cdleme41sn4aw  41641  cdlemeg46gfre  41698  cdlemf1  41727  cdlemg1cex  41754  cdlemg2ce  41758  cdlemg4d  41779  cdlemg4e  41780  cdlemg4f  41781  cdlemg4  41783  cdlemg6d  41787  cdlemg6e  41788  cdlemg7fvN  41790  cdlemg8b  41794  cdlemg8c  41795  cdlemg9a  41798  cdlemg9b  41799  cdlemg9  41800  cdlemg11aq  41804  cdlemg10a  41806  cdlemg12a  41809  cdlemg12b  41810  cdlemg12c  41811  cdlemg12d  41812  cdlemg13  41818  cdlemg14f  41819  cdlemg14g  41820  cdlemg17b  41828  cdlemg17dN  41829  cdlemg17e  41831  cdlemg17i  41835  cdlemg17pq  41838  cdlemg17iqN  41840  cdlemg18c  41846  cdlemg18d  41847  cdlemg18  41848  cdlemg19  41850  cdlemg21  41852  cdlemg27a  41858  cdlemg31b0N  41860  cdlemg27b  41862  cdlemg31c  41865  cdlemg33b0  41867  cdlemg33c0  41868  cdlemg33  41877  cdlemg35  41879  cdlemg43  41896  cdlemg44a  41897  cdlemg46  41901  cdlemh2  41982  cdlemh  41983  cdlemj1  41987  cdlemk3  41999  cdlemk5  42002  cdlemk6  42003  cdlemki  42007  cdlemksv2  42013  cdlemk12  42016  cdlemk15  42021  cdlemk16  42023  cdlemk18  42034  cdlemk19  42035  cdlemk7u  42036  cdlemk12u  42038  cdlemkoatnle-2N  42041  cdlemk13-2N  42042  cdlemkole-2N  42043  cdlemk14-2N  42044  cdlemk15-2N  42045  cdlemk16-2N  42046  cdlemk17-2N  42047  cdlemk18-2N  42052  cdlemk19-2N  42053  cdlemk7u-2N  42054  cdlemk11u-2N  42055  cdlemk12u-2N  42056  cdlemk20-2N  42058  cdlemk22  42059  cdlemk30  42060  cdlemk31  42062  cdlemk24-3  42069  cdlemkid2  42090  cdlemkfid3N  42091  cdlemk11ta  42095  cdlemkid3N  42099  cdlemk11tc  42111  cdlemk45  42113  cdlemk46  42114  cdlemk47  42115  cdlemk52  42120  cdlemk53a  42121  cdlemk53b  42122  cdleml1N  42142  cdleml3N  42144  cdlemn7  42369  cdlemn10  42372  dihordlem7  42380  dihord1  42384  dihord11c  42390  dihord2  42393  hlhilphllem  43125  fmuldfeq  46703  seposep  50148  iscnrm3rlem8  50169  iscnrm3llem2  50172