Theorem simp11 1204

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp11	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Proof of Theorem simp11

Step	Hyp	Ref	Expression
1		simp1 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	3ad2ant1 1133	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp111  1303  simp211  1312  simp311  1321  omeulem1  8507  omeu  8510  ackbij1lem16  10147  coprimeprodsq  16738  pythagtriplem14  16758  pythagtrip  16764  mrelatglb  18484  subglsm  19570  lsmpropd  19574  mdetmul  22526  decpmatid  22673  isfil2  23759  filuni  23788  cxple2a  26624  isosctr  26747  nolesgn2o  27599  nolesgn2ores  27600  nogesgn1o  27601  nogesgn1ores  27602  nolt02o  27623  nogt01o  27624  sslttr  27736  cofcut2  27853  brbtwn2  28868  colinearalg  28873  ax5seglem3  28894  clwwlknonex2  30071  measres  34188  bayesth  34406  ofscom  35980  btwndiff  36000  ifscgr  36017  brofs2  36050  brifs2  36051  fscgr  36053  btwnconn1lem1  36060  btwnconn1lem2  36061  btwnconn1lem3  36062  btwnconn1lem4  36063  btwnconn1lem5  36064  btwnconn1lem6  36065  btwnconn1lem7  36066  btwnconn1lem8  36067  btwnconn1lem9  36068  btwnconn1lem10  36069  btwnconn1lem11  36070  btwnconn1lem12  36071  seglecgr12im  36083  seglecgr12  36084  ivthALT  36308  eqlkr  39077  lkrshp  39083  lshpkrlem5  39092  cvrval3  39392  4noncolr3  39432  4noncolr2  39433  4noncolr1  39434  athgt  39435  3dimlem2  39438  3dimlem3a  39439  3dimlem4a  39442  3dimlem4  39443  3dimlem4OLDN  39444  3dim2  39447  1cvratex  39452  hlatexch4  39460  ps-2b  39461  3atlem1  39462  3atlem2  39463  3atlem4  39465  3atlem5  39466  3atlem6  39467  llnnleat  39492  2atm  39506  ps-2c  39507  llnmlplnN  39518  lplnnlelln  39522  2atmat  39540  2llnjN  39546  lvoli2  39560  lvolnlelln  39563  4atlem3b  39577  4atlem9  39582  4atlem10a  39583  4atlem10  39585  4atlem11a  39586  4atlem11b  39587  4atlem12a  39589  4atlem12b  39590  4at  39592  4at2  39593  lplncvrlvol2  39594  2lplnj  39599  dalemswapyz  39635  dath2  39716  lneq2at  39757  2lnat  39763  cdlema1N  39770  cdlemb  39773  paddasslem15  39813  pmodlem1  39825  llnmod2i2  39842  llnexchb2lem  39847  llnexchb2  39848  dalawlem1  39850  dalawlem3  39852  dalawlem4  39853  dalawlem5  39854  dalawlem6  39855  dalawlem7  39856  dalawlem8  39857  dalawlem9  39858  dalawlem10  39859  dalawlem11  39860  dalawlem12  39861  dalawlem13  39862  dalawlem15  39864  dalaw  39865  osumcllem5N  39939  osumcllem6N  39940  osumcllem7N  39941  osumcllem9N  39943  osumcllem10N  39944  osumcllem11N  39945  pl42lem1N  39958  lhpexle3lem  39990  lhpmcvr5N  40006  lhp2atne  40013  lhp2at0ne  40015  4atexlemswapqr  40042  4atexlemex6  40053  ldilco  40095  ltrneq  40128  trlval2  40142  trlnidat  40152  cdlemd2  40178  cdlemd7  40183  cdlemd8  40184  cdleme7aa  40221  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme11c  40240  cdleme11e  40242  cdleme11l  40248  cdleme11  40249  cdleme14  40252  cdleme15a  40253  cdleme15c  40255  cdleme16b  40258  cdleme16c  40259  cdleme16d  40260  cdleme16e  40261  cdleme16f  40262  cdleme0nex  40269  cdleme18d  40274  cdleme19b  40283  cdleme19d  40285  cdleme19e  40286  cdleme20f  40293  cdleme20i  40296  cdleme20k  40298  cdleme20l1  40299  cdleme20l2  40300  cdleme20l  40301  cdleme20m  40302  cdleme21a  40304  cdleme21b  40305  cdleme21ct  40308  cdleme21d  40309  cdleme21e  40310  cdleme21f  40311  cdleme21h  40313  cdleme22eALTN  40324  cdleme22f2  40326  cdleme22g  40327  cdleme26e  40338  cdleme26eALTN  40340  cdleme26fALTN  40341  cdleme26f  40342  cdleme26f2ALTN  40343  cdleme26f2  40344  cdleme28a  40349  cdleme28b  40350  cdleme28  40352  cdleme29ex  40353  cdleme29c  40355  cdlemefrs29cpre1  40377  cdlemefr29exN  40381  cdlemefr32sn2aw  40383  cdlemefr29bpre0N  40385  cdlemefr29clN  40386  cdlemefr32fvaN  40388  cdlemefr32fva1  40389  cdlemefs32sn1aw  40393  cdleme43fsv1snlem  40399  cdleme41sn3a  40412  cdleme32fva  40416  cdleme32b  40421  cdleme32d  40423  cdleme32e  40424  cdleme32f  40425  cdleme32le  40426  cdleme35a  40427  cdleme35fnpq  40428  cdleme35b  40429  cdleme35c  40430  cdleme35d  40431  cdleme35e  40432  cdleme35f  40433  cdleme36a  40439  cdleme36m  40440  cdleme37m  40441  cdleme39a  40444  cdleme39n  40445  cdleme40m  40446  cdleme40n  40447  cdleme42e  40458  cdleme42f  40459  cdleme42g  40460  cdleme43bN  40469  cdleme43cN  40470  cdleme43dN  40471  cdleme46f2g2  40472  cdleme46f2g1  40473  cdleme17d2  40474  cdleme48b  40482  cdleme4gfv  40486  cdlemeg49le  40490  cdlemeg46c  40492  cdlemeg46fvaw  40495  cdlemeg46nlpq  40496  cdlemeg46frv  40504  cdlemeg46rgv  40507  cdlemeg46req  40508  cdlemeg46gfre  40511  cdleme50trn1  40528  cdleme50trn2a  40529  cdleme50trn2  40530  cdleme  40539  cdlemf  40542  trlord  40548  cdlemg2ce  40571  cdlemg7fvbwN  40586  cdlemg7aN  40604  cdlemg10bALTN  40615  cdlemg10a  40619  cdlemg10  40620  cdlemg12d  40625  cdlemg12f  40627  cdlemg12g  40628  cdlemg12  40629  cdlemg13a  40630  cdlemg13  40631  cdlemg17b  40641  cdlemg17dN  40642  cdlemg17dALTN  40643  cdlemg17e  40644  cdlemg17f  40645  cdlemg17g  40646  cdlemg17h  40647  cdlemg17i  40648  cdlemg17pq  40651  cdlemg17bq  40652  cdlemg17iqN  40653  cdlemg17  40656  cdlemg18d  40660  cdlemg18  40661  cdlemg19a  40662  cdlemg19  40663  cdlemg21  40665  cdlemg27a  40671  cdlemg28a  40672  cdlemg31b0N  40673  cdlemg27b  40675  cdlemg33b0  40680  cdlemg28b  40682  cdlemg28  40683  cdlemg33a  40685  cdlemg33  40690  cdlemg34  40691  cdlemg35  40692  cdlemg36  40693  ltrnco  40698  trlcone  40707  cdlemg44  40712  cdlemg47  40715  cdlemg48  40716  tendococl  40751  tendoplcl  40760  cdlemh1  40794  cdlemi  40799  cdlemj1  40800  cdlemj2  40801  tendocan  40803  cdlemk6  40816  cdlemki  40820  cdlemksat  40825  cdlemksv2  40826  cdlemk7  40827  cdlemk11  40828  cdlemk12  40829  cdlemkoatnle  40830  cdlemkole  40832  cdlemk14  40833  cdlemk15  40834  cdlemk16a  40835  cdlemk16  40836  cdlemk17  40837  cdlemk1u  40838  cdlemk5u  40840  cdlemk6u  40841  cdlemkuat  40845  cdlemk18  40847  cdlemk19  40848  cdlemk12u  40851  cdlemk21N  40852  cdlemk20  40853  cdlemkoatnle-2N  40854  cdlemk13-2N  40855  cdlemkole-2N  40856  cdlemk14-2N  40857  cdlemk15-2N  40858  cdlemk16-2N  40859  cdlemk17-2N  40860  cdlemk18-2N  40865  cdlemk19-2N  40866  cdlemk7u-2N  40867  cdlemk11u-2N  40868  cdlemk12u-2N  40869  cdlemk21-2N  40870  cdlemk20-2N  40871  cdlemk22  40872  cdlemk23-3  40881  cdlemk25-3  40883  cdlemk26b-3  40884  cdlemk27-3  40886  cdlemk28-3  40887  cdlemk33N  40888  cdlemk37  40893  cdlemky  40905  cdlemk11ta  40908  cdlemkid3N  40912  cdlemk11tc  40924  cdlemk11t  40925  cdlemk45  40926  cdlemk46  40927  cdlemk47  40928  cdlemk48  40929  cdlemk49  40930  cdlemk50  40931  cdlemk51  40932  cdlemk52  40933  cdlemk55b  40939  cdlemkyyN  40941  cdlemk55u1  40944  cdlemk55u  40945  cdlemk39u1  40946  cdlemk39u  40947  cdlemk56  40950  cdleml3N  40957  cdleml4N  40958  cdlemm10N  41097  dihord1  41197  dihord2a  41198  dihord2b  41199  dihord10  41202  dihord11c  41203  dihord2pre  41204  dihord4  41237  dihord5apre  41241  dihmeetlem1N  41269  dihglbcpreN  41279  dihjatc1  41290  dihjatc3  41292  dihmeetlem13N  41298  dihmeetlem20N  41305  baerlem3lem2  41689  baerlem5alem2  41690  baerlem5blem2  41691  hdmap14lem11  41857  hdmap14lem12  41858  flt4lem5  42623  monotuz  42914  congmul  42940  congsub  42943  rpnnen3lem  43004  ntrclsiso  44040  ntrclskb  44042  ntrclsk3  44043  wessf1ornlem  45163  infleinf  45352  lincdifsn  48410  itsclc0yqe  48747  itsclc0xyqsolr  48755  iscnrm3rlem8  48932  iscnrm3llem2  48935