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  7363  smogt  8356  frlmphl  21994  mdetuni0  22843  mdetmul  22845  gsummatr01lem3  22879  decpmatmullem  22996  tsmsxp  24381  log2sumbnd  27780  nosupres  27943  noinfres  27958  ax5seg  29395  wlkoniswlk  30119  iocinioc2  33250  totprob  34938  cgrtr  36572  cgrtr3  36574  ofscom  36587  cgrextend  36588  segconeq  36590  ifscgr  36624  btwnxfr  36636  colinearxfr  36655  brofs2  36657  brifs2  36658  fscgr  36660  btwnconn1lem1  36667  btwnconn1lem2  36668  btwnconn1lem5  36671  btwnconn1lem6  36672  btwnconn1lem7  36673  btwnconn1lem8  36674  btwnconn1lem9  36675  btwnconn1lem10  36676  btwnconn1lem11  36677  btwnconn1lem12  36678  seglecgr12im  36690  seglecgr12  36691  segletr  36694  outsideofeq  36710  ivthALT  36954  lshpkrlem5  39987  lshpkrlem6  39988  exatleN  40277  atbtwn  40319  atbtwnexOLDN  40320  atbtwnex  40321  4noncolr3  40326  3dimlem3a  40333  3dimlem4a  40336  3dim1  40340  3dim2  40341  1cvrat  40349  2atjlej  40352  hlatexch4  40354  ps-2b  40355  2atm  40400  2atmat  40434  4atlem11b  40481  4atlem11  40482  4at  40486  4at2  40487  2lplnja  40492  2lplnj  40493  dalemswapyz  40529  dalemccnedd  40560  cdlemb  40667  paddasslem5  40697  paddasslem15  40707  pmodlem1  40719  dalawlem1  40744  dalawlem3  40746  dalawlem4  40747  dalawlem5  40748  dalawlem6  40749  dalawlem7  40750  dalawlem8  40751  dalawlem9  40752  dalawlem11  40754  dalawlem12  40755  dalawlem15  40758  osumcllem5N  40833  osumcllem6N  40834  lhpexle3lem  40884  lhpmcvr4N  40899  lhpmcvr6N  40901  4atex2  40950  4atex2-0bOLDN  40952  4atex3  40954  ltrn11at  41020  trlval3  41060  cdlemd3  41073  cdleme0moN  41098  cdleme7aa  41115  cdleme7b  41117  cdleme7c  41118  cdleme7d  41119  cdleme7e  41120  cdleme7ga  41121  cdleme7  41122  cdleme16aN  41132  cdleme11dN  41135  cdleme11e  41136  cdleme11l  41142  cdleme11  41143  cdleme12  41144  cdleme14  41146  cdleme15b  41148  cdleme15c  41149  cdleme16b  41152  cdleme16c  41153  cdleme16d  41154  cdleme16e  41155  cdleme16f  41156  cdleme17c  41161  cdleme18c  41166  cdleme18d  41168  cdlemeda  41171  cdleme19a  41176  cdleme19b  41177  cdleme19c  41178  cdleme20aN  41182  cdleme20bN  41183  cdleme20d  41185  cdleme20i  41190  cdleme20j  41191  cdleme20l1  41193  cdleme20l2  41194  cdleme21d  41203  cdleme21e  41204  cdleme21f  41205  cdleme22aa  41212  cdleme22e  41217  cdleme22eALTN  41218  cdleme22f2  41220  cdleme22g  41221  cdleme23b  41223  cdleme26eALTN  41234  cdleme26fALTN  41235  cdleme26f  41236  cdleme26f2ALTN  41237  cdleme26f2  41238  cdleme28a  41243  cdleme28b  41244  cdleme32b  41315  cdleme32c  41316  cdleme32e  41318  cdleme35h  41329  cdleme35sn2aw  41331  cdleme41sn3aw  41347  cdleme41sn4aw  41348  cdlemeg46gfre  41405  cdlemf1  41434  cdlemg1cex  41461  cdlemg2ce  41465  cdlemg4d  41486  cdlemg4e  41487  cdlemg4f  41488  cdlemg4  41490  cdlemg6d  41494  cdlemg6e  41495  cdlemg7fvN  41497  cdlemg8b  41501  cdlemg8c  41502  cdlemg9a  41505  cdlemg9b  41506  cdlemg9  41507  cdlemg11aq  41511  cdlemg10a  41513  cdlemg12a  41516  cdlemg12b  41517  cdlemg12c  41518  cdlemg12d  41519  cdlemg13  41525  cdlemg14f  41526  cdlemg14g  41527  cdlemg17b  41535  cdlemg17dN  41536  cdlemg17e  41538  cdlemg17i  41542  cdlemg17pq  41545  cdlemg17iqN  41547  cdlemg18c  41553  cdlemg18d  41554  cdlemg18  41555  cdlemg19  41557  cdlemg21  41559  cdlemg27a  41565  cdlemg31b0N  41567  cdlemg27b  41569  cdlemg31c  41572  cdlemg33b0  41574  cdlemg33c0  41575  cdlemg33  41584  cdlemg35  41586  cdlemg43  41603  cdlemg44a  41604  cdlemg46  41608  cdlemh2  41689  cdlemh  41690  cdlemj1  41694  cdlemk3  41706  cdlemk5  41709  cdlemk6  41710  cdlemki  41714  cdlemksv2  41720  cdlemk12  41723  cdlemk15  41728  cdlemk16  41730  cdlemk18  41741  cdlemk19  41742  cdlemk7u  41743  cdlemk12u  41745  cdlemkoatnle-2N  41748  cdlemk13-2N  41749  cdlemkole-2N  41750  cdlemk14-2N  41751  cdlemk15-2N  41752  cdlemk16-2N  41753  cdlemk17-2N  41754  cdlemk18-2N  41759  cdlemk19-2N  41760  cdlemk7u-2N  41761  cdlemk11u-2N  41762  cdlemk12u-2N  41763  cdlemk20-2N  41765  cdlemk22  41766  cdlemk30  41767  cdlemk31  41769  cdlemk24-3  41776  cdlemkid2  41797  cdlemkfid3N  41798  cdlemk11ta  41802  cdlemkid3N  41806  cdlemk11tc  41818  cdlemk45  41820  cdlemk46  41821  cdlemk47  41822  cdlemk52  41827  cdlemk53a  41828  cdlemk53b  41829  cdleml1N  41849  cdleml3N  41851  cdlemn7  42076  cdlemn10  42079  dihordlem7  42087  dihord1  42091  dihord11c  42097  dihord2  42100  hlhilphllem  42832  fmuldfeq  46413  seposep  49852  iscnrm3rlem8  49873  iscnrm3llem2  49876