Theorem simp31 1205

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp131  1304  simp231  1313  simp331  1322  smogt  8006  frlmphl  20927  mdetuni0  21232  mdetmul  21234  gsummatr01lem3  21268  decpmatmullem  21381  tsmsxp  22765  log2sumbnd  26122  ax5seg  26726  wlkoniswlk  27445  iocinioc2  30504  totprob  31687  eqfunresadj  33006  nosupres  33209  cgrtr  33455  cgrtr3  33457  ofscom  33470  cgrextend  33471  segconeq  33473  ifscgr  33507  btwnxfr  33519  colinearxfr  33538  brofs2  33540  brifs2  33541  fscgr  33543  btwnconn1lem1  33550  btwnconn1lem2  33551  btwnconn1lem5  33554  btwnconn1lem6  33555  btwnconn1lem7  33556  btwnconn1lem8  33557  btwnconn1lem9  33558  btwnconn1lem10  33559  btwnconn1lem11  33560  btwnconn1lem12  33561  seglecgr12im  33573  seglecgr12  33574  segletr  33577  outsideofeq  33593  ivthALT  33685  lshpkrlem5  36252  lshpkrlem6  36253  exatleN  36542  atbtwn  36584  atbtwnexOLDN  36585  atbtwnex  36586  4noncolr3  36591  3dimlem3a  36598  3dimlem4a  36601  3dim1  36605  3dim2  36606  1cvrat  36614  2atjlej  36617  hlatexch4  36619  ps-2b  36620  2atm  36665  2atmat  36699  4atlem11b  36746  4atlem11  36747  4at  36751  4at2  36752  2lplnja  36757  2lplnj  36758  dalemswapyz  36794  dalemccnedd  36825  cdlemb  36932  paddasslem5  36962  paddasslem15  36972  pmodlem1  36984  dalawlem1  37009  dalawlem3  37011  dalawlem4  37012  dalawlem5  37013  dalawlem6  37014  dalawlem7  37015  dalawlem8  37016  dalawlem9  37017  dalawlem11  37019  dalawlem12  37020  dalawlem15  37023  osumcllem5N  37098  osumcllem6N  37099  lhpexle3lem  37149  lhpmcvr4N  37164  lhpmcvr6N  37166  4atex2  37215  4atex2-0bOLDN  37217  4atex3  37219  ltrn11at  37285  trlval3  37325  cdlemd3  37338  cdleme0moN  37363  cdleme7aa  37380  cdleme7b  37382  cdleme7c  37383  cdleme7d  37384  cdleme7e  37385  cdleme7ga  37386  cdleme7  37387  cdleme16aN  37397  cdleme11dN  37400  cdleme11e  37401  cdleme11l  37407  cdleme11  37408  cdleme12  37409  cdleme14  37411  cdleme15b  37413  cdleme15c  37414  cdleme16b  37417  cdleme16c  37418  cdleme16d  37419  cdleme16e  37420  cdleme16f  37421  cdleme17c  37426  cdleme18c  37431  cdleme18d  37433  cdlemeda  37436  cdleme19a  37441  cdleme19b  37442  cdleme19c  37443  cdleme20aN  37447  cdleme20bN  37448  cdleme20d  37450  cdleme20i  37455  cdleme20j  37456  cdleme20l1  37458  cdleme20l2  37459  cdleme21d  37468  cdleme21e  37469  cdleme21f  37470  cdleme22aa  37477  cdleme22e  37482  cdleme22eALTN  37483  cdleme22f2  37485  cdleme22g  37486  cdleme23b  37488  cdleme26eALTN  37499  cdleme26fALTN  37500  cdleme26f  37501  cdleme26f2ALTN  37502  cdleme26f2  37503  cdleme28a  37508  cdleme28b  37509  cdleme32b  37580  cdleme32c  37581  cdleme32e  37583  cdleme35h  37594  cdleme35sn2aw  37596  cdleme41sn3aw  37612  cdleme41sn4aw  37613  cdlemeg46gfre  37670  cdlemf1  37699  cdlemg1cex  37726  cdlemg2ce  37730  cdlemg4d  37751  cdlemg4e  37752  cdlemg4f  37753  cdlemg4  37755  cdlemg6d  37759  cdlemg6e  37760  cdlemg7fvN  37762  cdlemg8b  37766  cdlemg8c  37767  cdlemg9a  37770  cdlemg9b  37771  cdlemg9  37772  cdlemg11aq  37776  cdlemg10a  37778  cdlemg12a  37781  cdlemg12b  37782  cdlemg12c  37783  cdlemg12d  37784  cdlemg13  37790  cdlemg14f  37791  cdlemg14g  37792  cdlemg17b  37800  cdlemg17dN  37801  cdlemg17e  37803  cdlemg17i  37807  cdlemg17pq  37810  cdlemg17iqN  37812  cdlemg18c  37818  cdlemg18d  37819  cdlemg18  37820  cdlemg19  37822  cdlemg21  37824  cdlemg27a  37830  cdlemg31b0N  37832  cdlemg27b  37834  cdlemg31c  37837  cdlemg33b0  37839  cdlemg33c0  37840  cdlemg33  37849  cdlemg35  37851  cdlemg43  37868  cdlemg44a  37869  cdlemg46  37873  cdlemh2  37954  cdlemh  37955  cdlemj1  37959  cdlemk3  37971  cdlemk5  37974  cdlemk6  37975  cdlemki  37979  cdlemksv2  37985  cdlemk12  37988  cdlemk15  37993  cdlemk16  37995  cdlemk18  38006  cdlemk19  38007  cdlemk7u  38008  cdlemk12u  38010  cdlemkoatnle-2N  38013  cdlemk13-2N  38014  cdlemkole-2N  38015  cdlemk14-2N  38016  cdlemk15-2N  38017  cdlemk16-2N  38018  cdlemk17-2N  38019  cdlemk18-2N  38024  cdlemk19-2N  38025  cdlemk7u-2N  38026  cdlemk11u-2N  38027  cdlemk12u-2N  38028  cdlemk20-2N  38030  cdlemk22  38031  cdlemk30  38032  cdlemk31  38034  cdlemk24-3  38041  cdlemkid2  38062  cdlemkfid3N  38063  cdlemk11ta  38067  cdlemkid3N  38071  cdlemk11tc  38083  cdlemk45  38085  cdlemk46  38086  cdlemk47  38087  cdlemk52  38092  cdlemk53a  38093  cdlemk53b  38094  cdleml1N  38114  cdleml3N  38116  cdlemn7  38341  cdlemn10  38344  dihordlem7  38352  dihord1  38356  dihord11c  38362  dihord2  38365  hlhilphllem  39097  fmuldfeq  41871