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  7370  smogt  8376  frlmphl  22088  mdetuni0  22937  mdetmul  22939  gsummatr01lem3  22973  decpmatmullem  23090  tsmsxp  24475  log2sumbnd  27872  nosupres  28065  noinfres  28080  ax5seg  29517  wlkoniswlk  30241  iocinioc2  33414  totprob  35102  cgrtr  36832  cgrtr3  36834  ofscom  36847  cgrextend  36848  segconeq  36850  ifscgr  36884  btwnxfr  36896  colinearxfr  36915  brofs2  36917  brifs2  36918  fscgr  36920  btwnconn1lem1  36927  btwnconn1lem2  36928  btwnconn1lem5  36931  btwnconn1lem6  36932  btwnconn1lem7  36933  btwnconn1lem8  36934  btwnconn1lem9  36935  btwnconn1lem10  36936  btwnconn1lem11  36937  btwnconn1lem12  36938  seglecgr12im  36950  seglecgr12  36951  segletr  36954  outsideofeq  36970  ivthALT  37198  lshpkrlem5  40247  lshpkrlem6  40248  exatleN  40537  atbtwn  40579  atbtwnexOLDN  40580  atbtwnex  40581  4noncolr3  40586  3dimlem3a  40593  3dimlem4a  40596  3dim1  40600  3dim2  40601  1cvrat  40609  2atjlej  40612  hlatexch4  40614  ps-2b  40615  2atm  40660  2atmat  40694  4atlem11b  40741  4atlem11  40742  4at  40746  4at2  40747  2lplnja  40752  2lplnj  40753  dalemswapyz  40789  dalemccnedd  40820  cdlemb  40927  paddasslem5  40957  paddasslem15  40967  pmodlem1  40979  dalawlem1  41004  dalawlem3  41006  dalawlem4  41007  dalawlem5  41008  dalawlem6  41009  dalawlem7  41010  dalawlem8  41011  dalawlem9  41012  dalawlem11  41014  dalawlem12  41015  dalawlem15  41018  osumcllem5N  41093  osumcllem6N  41094  lhpexle3lem  41144  lhpmcvr4N  41159  lhpmcvr6N  41161  4atex2  41210  4atex2-0bOLDN  41212  4atex3  41214  ltrn11at  41280  trlval3  41320  cdlemd3  41333  cdleme0moN  41358  cdleme7aa  41375  cdleme7b  41377  cdleme7c  41378  cdleme7d  41379  cdleme7e  41380  cdleme7ga  41381  cdleme7  41382  cdleme16aN  41392  cdleme11dN  41395  cdleme11e  41396  cdleme11l  41402  cdleme11  41403  cdleme12  41404  cdleme14  41406  cdleme15b  41408  cdleme15c  41409  cdleme16b  41412  cdleme16c  41413  cdleme16d  41414  cdleme16e  41415  cdleme16f  41416  cdleme17c  41421  cdleme18c  41426  cdleme18d  41428  cdlemeda  41431  cdleme19a  41436  cdleme19b  41437  cdleme19c  41438  cdleme20aN  41442  cdleme20bN  41443  cdleme20d  41445  cdleme20i  41450  cdleme20j  41451  cdleme20l1  41453  cdleme20l2  41454  cdleme21d  41463  cdleme21e  41464  cdleme21f  41465  cdleme22aa  41472  cdleme22e  41477  cdleme22eALTN  41478  cdleme22f2  41480  cdleme22g  41481  cdleme23b  41483  cdleme26eALTN  41494  cdleme26fALTN  41495  cdleme26f  41496  cdleme26f2ALTN  41497  cdleme26f2  41498  cdleme28a  41503  cdleme28b  41504  cdleme32b  41575  cdleme32c  41576  cdleme32e  41578  cdleme35h  41589  cdleme35sn2aw  41591  cdleme41sn3aw  41607  cdleme41sn4aw  41608  cdlemeg46gfre  41665  cdlemf1  41694  cdlemg1cex  41721  cdlemg2ce  41725  cdlemg4d  41746  cdlemg4e  41747  cdlemg4f  41748  cdlemg4  41750  cdlemg6d  41754  cdlemg6e  41755  cdlemg7fvN  41757  cdlemg8b  41761  cdlemg8c  41762  cdlemg9a  41765  cdlemg9b  41766  cdlemg9  41767  cdlemg11aq  41771  cdlemg10a  41773  cdlemg12a  41776  cdlemg12b  41777  cdlemg12c  41778  cdlemg12d  41779  cdlemg13  41785  cdlemg14f  41786  cdlemg14g  41787  cdlemg17b  41795  cdlemg17dN  41796  cdlemg17e  41798  cdlemg17i  41802  cdlemg17pq  41805  cdlemg17iqN  41807  cdlemg18c  41813  cdlemg18d  41814  cdlemg18  41815  cdlemg19  41817  cdlemg21  41819  cdlemg27a  41825  cdlemg31b0N  41827  cdlemg27b  41829  cdlemg31c  41832  cdlemg33b0  41834  cdlemg33c0  41835  cdlemg33  41844  cdlemg35  41846  cdlemg43  41863  cdlemg44a  41864  cdlemg46  41868  cdlemh2  41949  cdlemh  41950  cdlemj1  41954  cdlemk3  41966  cdlemk5  41969  cdlemk6  41970  cdlemki  41974  cdlemksv2  41980  cdlemk12  41983  cdlemk15  41988  cdlemk16  41990  cdlemk18  42001  cdlemk19  42002  cdlemk7u  42003  cdlemk12u  42005  cdlemkoatnle-2N  42008  cdlemk13-2N  42009  cdlemkole-2N  42010  cdlemk14-2N  42011  cdlemk15-2N  42012  cdlemk16-2N  42013  cdlemk17-2N  42014  cdlemk18-2N  42019  cdlemk19-2N  42020  cdlemk7u-2N  42021  cdlemk11u-2N  42022  cdlemk12u-2N  42023  cdlemk20-2N  42025  cdlemk22  42026  cdlemk30  42027  cdlemk31  42029  cdlemk24-3  42036  cdlemkid2  42057  cdlemkfid3N  42058  cdlemk11ta  42062  cdlemkid3N  42066  cdlemk11tc  42078  cdlemk45  42080  cdlemk46  42081  cdlemk47  42082  cdlemk52  42087  cdlemk53a  42088  cdlemk53b  42089  cdleml1N  42109  cdleml3N  42111  cdlemn7  42336  cdlemn10  42339  dihordlem7  42347  dihord1  42351  dihord11c  42357  dihord2  42360  hlhilphllem  43092  fmuldfeq  46671  seposep  50110  iscnrm3rlem8  50131  iscnrm3llem2  50134