Theorem simp31 1222

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  simp131  1321  simp231  1330  simp331  1339  eqfunresadj  7339  smogt  8332  frlmphl  21821  mdetuni0  22669  mdetmul  22671  gsummatr01lem3  22705  decpmatmullem  22819  tsmsxp  24203  log2sumbnd  27596  nosupres  27759  noinfres  27774  ax5seg  29096  wlkoniswlk  29817  iocinioc2  32942  totprob  34685  cgrtr  36303  cgrtr3  36305  ofscom  36318  cgrextend  36319  segconeq  36321  ifscgr  36355  btwnxfr  36367  colinearxfr  36386  brofs2  36388  brifs2  36389  fscgr  36391  btwnconn1lem1  36398  btwnconn1lem2  36399  btwnconn1lem5  36402  btwnconn1lem6  36403  btwnconn1lem7  36404  btwnconn1lem8  36405  btwnconn1lem9  36406  btwnconn1lem10  36407  btwnconn1lem11  36408  btwnconn1lem12  36409  seglecgr12im  36421  seglecgr12  36422  segletr  36425  outsideofeq  36441  ivthALT  36656  lshpkrlem5  39699  lshpkrlem6  39700  exatleN  39989  atbtwn  40031  atbtwnexOLDN  40032  atbtwnex  40033  4noncolr3  40038  3dimlem3a  40045  3dimlem4a  40048  3dim1  40052  3dim2  40053  1cvrat  40061  2atjlej  40064  hlatexch4  40066  ps-2b  40067  2atm  40112  2atmat  40146  4atlem11b  40193  4atlem11  40194  4at  40198  4at2  40199  2lplnja  40204  2lplnj  40205  dalemswapyz  40241  dalemccnedd  40272  cdlemb  40379  paddasslem5  40409  paddasslem15  40419  pmodlem1  40431  dalawlem1  40456  dalawlem3  40458  dalawlem4  40459  dalawlem5  40460  dalawlem6  40461  dalawlem7  40462  dalawlem8  40463  dalawlem9  40464  dalawlem11  40466  dalawlem12  40467  dalawlem15  40470  osumcllem5N  40545  osumcllem6N  40546  lhpexle3lem  40596  lhpmcvr4N  40611  lhpmcvr6N  40613  4atex2  40662  4atex2-0bOLDN  40664  4atex3  40666  ltrn11at  40732  trlval3  40772  cdlemd3  40785  cdleme0moN  40810  cdleme7aa  40827  cdleme7b  40829  cdleme7c  40830  cdleme7d  40831  cdleme7e  40832  cdleme7ga  40833  cdleme7  40834  cdleme16aN  40844  cdleme11dN  40847  cdleme11e  40848  cdleme11l  40854  cdleme11  40855  cdleme12  40856  cdleme14  40858  cdleme15b  40860  cdleme15c  40861  cdleme16b  40864  cdleme16c  40865  cdleme16d  40866  cdleme16e  40867  cdleme16f  40868  cdleme17c  40873  cdleme18c  40878  cdleme18d  40880  cdlemeda  40883  cdleme19a  40888  cdleme19b  40889  cdleme19c  40890  cdleme20aN  40894  cdleme20bN  40895  cdleme20d  40897  cdleme20i  40902  cdleme20j  40903  cdleme20l1  40905  cdleme20l2  40906  cdleme21d  40915  cdleme21e  40916  cdleme21f  40917  cdleme22aa  40924  cdleme22e  40929  cdleme22eALTN  40930  cdleme22f2  40932  cdleme22g  40933  cdleme23b  40935  cdleme26eALTN  40946  cdleme26fALTN  40947  cdleme26f  40948  cdleme26f2ALTN  40949  cdleme26f2  40950  cdleme28a  40955  cdleme28b  40956  cdleme32b  41027  cdleme32c  41028  cdleme32e  41030  cdleme35h  41041  cdleme35sn2aw  41043  cdleme41sn3aw  41059  cdleme41sn4aw  41060  cdlemeg46gfre  41117  cdlemf1  41146  cdlemg1cex  41173  cdlemg2ce  41177  cdlemg4d  41198  cdlemg4e  41199  cdlemg4f  41200  cdlemg4  41202  cdlemg6d  41206  cdlemg6e  41207  cdlemg7fvN  41209  cdlemg8b  41213  cdlemg8c  41214  cdlemg9a  41217  cdlemg9b  41218  cdlemg9  41219  cdlemg11aq  41223  cdlemg10a  41225  cdlemg12a  41228  cdlemg12b  41229  cdlemg12c  41230  cdlemg12d  41231  cdlemg13  41237  cdlemg14f  41238  cdlemg14g  41239  cdlemg17b  41247  cdlemg17dN  41248  cdlemg17e  41250  cdlemg17i  41254  cdlemg17pq  41257  cdlemg17iqN  41259  cdlemg18c  41265  cdlemg18d  41266  cdlemg18  41267  cdlemg19  41269  cdlemg21  41271  cdlemg27a  41277  cdlemg31b0N  41279  cdlemg27b  41281  cdlemg31c  41284  cdlemg33b0  41286  cdlemg33c0  41287  cdlemg33  41296  cdlemg35  41298  cdlemg43  41315  cdlemg44a  41316  cdlemg46  41320  cdlemh2  41401  cdlemh  41402  cdlemj1  41406  cdlemk3  41418  cdlemk5  41421  cdlemk6  41422  cdlemki  41426  cdlemksv2  41432  cdlemk12  41435  cdlemk15  41440  cdlemk16  41442  cdlemk18  41453  cdlemk19  41454  cdlemk7u  41455  cdlemk12u  41457  cdlemkoatnle-2N  41460  cdlemk13-2N  41461  cdlemkole-2N  41462  cdlemk14-2N  41463  cdlemk15-2N  41464  cdlemk16-2N  41465  cdlemk17-2N  41466  cdlemk18-2N  41471  cdlemk19-2N  41472  cdlemk7u-2N  41473  cdlemk11u-2N  41474  cdlemk12u-2N  41475  cdlemk20-2N  41477  cdlemk22  41478  cdlemk30  41479  cdlemk31  41481  cdlemk24-3  41488  cdlemkid2  41509  cdlemkfid3N  41510  cdlemk11ta  41514  cdlemkid3N  41518  cdlemk11tc  41530  cdlemk45  41532  cdlemk46  41533  cdlemk47  41534  cdlemk52  41539  cdlemk53a  41540  cdlemk53b  41541  cdleml1N  41561  cdleml3N  41563  cdlemn7  41788  cdlemn10  41791  dihordlem7  41799  dihord1  41803  dihord11c  41809  dihord2  41812  hlhilphllem  42544  fmuldfeq  46120  seposep  49508  iscnrm3rlem8  49529  iscnrm3llem2  49532