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  8509  omeu  8512  ackbij1lem16  10144  coprimeprodsq  16736  pythagtriplem14  16756  pythagtrip  16762  mrelatglb  18483  subglsm  19602  lsmpropd  19606  mdetmul  22567  decpmatid  22714  isfil2  23800  filuni  23829  cxple2a  26664  isosctr  26787  nolesgn2o  27639  nolesgn2ores  27640  nogesgn1o  27641  nogesgn1ores  27642  nolt02o  27663  nogt01o  27664  sltstr  27783  cofcut2  27918  brbtwn2  28978  colinearalg  28983  ax5seglem3  29004  clwwlknonex2  30184  measres  34379  bayesth  34596  ofscom  36201  btwndiff  36221  ifscgr  36238  brofs2  36271  brifs2  36272  fscgr  36274  btwnconn1lem1  36281  btwnconn1lem2  36282  btwnconn1lem3  36283  btwnconn1lem4  36284  btwnconn1lem5  36285  btwnconn1lem6  36286  btwnconn1lem7  36287  btwnconn1lem8  36288  btwnconn1lem9  36289  btwnconn1lem10  36290  btwnconn1lem11  36291  btwnconn1lem12  36292  seglecgr12im  36304  seglecgr12  36305  ivthALT  36529  eqlkr  39355  lkrshp  39361  lshpkrlem5  39370  cvrval3  39669  4noncolr3  39709  4noncolr2  39710  4noncolr1  39711  athgt  39712  3dimlem2  39715  3dimlem3a  39716  3dimlem4a  39719  3dimlem4  39720  3dimlem4OLDN  39721  3dim2  39724  1cvratex  39729  hlatexch4  39737  ps-2b  39738  3atlem1  39739  3atlem2  39740  3atlem4  39742  3atlem5  39743  3atlem6  39744  llnnleat  39769  2atm  39783  ps-2c  39784  llnmlplnN  39795  lplnnlelln  39799  2atmat  39817  2llnjN  39823  lvoli2  39837  lvolnlelln  39840  4atlem3b  39854  4atlem9  39859  4atlem10a  39860  4atlem10  39862  4atlem11a  39863  4atlem11b  39864  4atlem12a  39866  4atlem12b  39867  4at  39869  4at2  39870  lplncvrlvol2  39871  2lplnj  39876  dalemswapyz  39912  dath2  39993  lneq2at  40034  2lnat  40040  cdlema1N  40047  cdlemb  40050  paddasslem15  40090  pmodlem1  40102  llnmod2i2  40119  llnexchb2lem  40124  llnexchb2  40125  dalawlem1  40127  dalawlem3  40129  dalawlem4  40130  dalawlem5  40131  dalawlem6  40132  dalawlem7  40133  dalawlem8  40134  dalawlem9  40135  dalawlem10  40136  dalawlem11  40137  dalawlem12  40138  dalawlem13  40139  dalawlem15  40141  dalaw  40142  osumcllem5N  40216  osumcllem6N  40217  osumcllem7N  40218  osumcllem9N  40220  osumcllem10N  40221  osumcllem11N  40222  pl42lem1N  40235  lhpexle3lem  40267  lhpmcvr5N  40283  lhp2atne  40290  lhp2at0ne  40292  4atexlemswapqr  40319  4atexlemex6  40330  ldilco  40372  ltrneq  40405  trlval2  40419  trlnidat  40429  cdlemd2  40455  cdlemd7  40460  cdlemd8  40461  cdleme7aa  40498  cdleme7c  40501  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme11c  40517  cdleme11e  40519  cdleme11l  40525  cdleme11  40526  cdleme14  40529  cdleme15a  40530  cdleme15c  40532  cdleme16b  40535  cdleme16c  40536  cdleme16d  40537  cdleme16e  40538  cdleme16f  40539  cdleme0nex  40546  cdleme18d  40551  cdleme19b  40560  cdleme19d  40562  cdleme19e  40563  cdleme20f  40570  cdleme20i  40573  cdleme20k  40575  cdleme20l1  40576  cdleme20l2  40577  cdleme20l  40578  cdleme20m  40579  cdleme21a  40581  cdleme21b  40582  cdleme21ct  40585  cdleme21d  40586  cdleme21e  40587  cdleme21f  40588  cdleme21h  40590  cdleme22eALTN  40601  cdleme22f2  40603  cdleme22g  40604  cdleme26e  40615  cdleme26eALTN  40617  cdleme26fALTN  40618  cdleme26f  40619  cdleme26f2ALTN  40620  cdleme26f2  40621  cdleme28a  40626  cdleme28b  40627  cdleme28  40629  cdleme29ex  40630  cdleme29c  40632  cdlemefrs29cpre1  40654  cdlemefr29exN  40658  cdlemefr32sn2aw  40660  cdlemefr29bpre0N  40662  cdlemefr29clN  40663  cdlemefr32fvaN  40665  cdlemefr32fva1  40666  cdlemefs32sn1aw  40670  cdleme43fsv1snlem  40676  cdleme41sn3a  40689  cdleme32fva  40693  cdleme32b  40698  cdleme32d  40700  cdleme32e  40701  cdleme32f  40702  cdleme32le  40703  cdleme35a  40704  cdleme35fnpq  40705  cdleme35b  40706  cdleme35c  40707  cdleme35d  40708  cdleme35e  40709  cdleme35f  40710  cdleme36a  40716  cdleme36m  40717  cdleme37m  40718  cdleme39a  40721  cdleme39n  40722  cdleme40m  40723  cdleme40n  40724  cdleme42e  40735  cdleme42f  40736  cdleme42g  40737  cdleme43bN  40746  cdleme43cN  40747  cdleme43dN  40748  cdleme46f2g2  40749  cdleme46f2g1  40750  cdleme17d2  40751  cdleme48b  40759  cdleme4gfv  40763  cdlemeg49le  40767  cdlemeg46c  40769  cdlemeg46fvaw  40772  cdlemeg46nlpq  40773  cdlemeg46frv  40781  cdlemeg46rgv  40784  cdlemeg46req  40785  cdlemeg46gfre  40788  cdleme50trn1  40805  cdleme50trn2a  40806  cdleme50trn2  40807  cdleme  40816  cdlemf  40819  trlord  40825  cdlemg2ce  40848  cdlemg7fvbwN  40863  cdlemg7aN  40881  cdlemg10bALTN  40892  cdlemg10a  40896  cdlemg10  40897  cdlemg12d  40902  cdlemg12f  40904  cdlemg12g  40905  cdlemg12  40906  cdlemg13a  40907  cdlemg13  40908  cdlemg17b  40918  cdlemg17dN  40919  cdlemg17dALTN  40920  cdlemg17e  40921  cdlemg17f  40922  cdlemg17g  40923  cdlemg17h  40924  cdlemg17i  40925  cdlemg17pq  40928  cdlemg17bq  40929  cdlemg17iqN  40930  cdlemg17  40933  cdlemg18d  40937  cdlemg18  40938  cdlemg19a  40939  cdlemg19  40940  cdlemg21  40942  cdlemg27a  40948  cdlemg28a  40949  cdlemg31b0N  40950  cdlemg27b  40952  cdlemg33b0  40957  cdlemg28b  40959  cdlemg28  40960  cdlemg33a  40962  cdlemg33  40967  cdlemg34  40968  cdlemg35  40969  cdlemg36  40970  ltrnco  40975  trlcone  40984  cdlemg44  40989  cdlemg47  40992  cdlemg48  40993  tendococl  41028  tendoplcl  41037  cdlemh1  41071  cdlemi  41076  cdlemj1  41077  cdlemj2  41078  tendocan  41080  cdlemk6  41093  cdlemki  41097  cdlemksat  41102  cdlemksv2  41103  cdlemk7  41104  cdlemk11  41105  cdlemk12  41106  cdlemkoatnle  41107  cdlemkole  41109  cdlemk14  41110  cdlemk15  41111  cdlemk16a  41112  cdlemk16  41113  cdlemk17  41114  cdlemk1u  41115  cdlemk5u  41117  cdlemk6u  41118  cdlemkuat  41122  cdlemk18  41124  cdlemk19  41125  cdlemk12u  41128  cdlemk21N  41129  cdlemk20  41130  cdlemkoatnle-2N  41131  cdlemk13-2N  41132  cdlemkole-2N  41133  cdlemk14-2N  41134  cdlemk15-2N  41135  cdlemk16-2N  41136  cdlemk17-2N  41137  cdlemk18-2N  41142  cdlemk19-2N  41143  cdlemk7u-2N  41144  cdlemk11u-2N  41145  cdlemk12u-2N  41146  cdlemk21-2N  41147  cdlemk20-2N  41148  cdlemk22  41149  cdlemk23-3  41158  cdlemk25-3  41160  cdlemk26b-3  41161  cdlemk27-3  41163  cdlemk28-3  41164  cdlemk33N  41165  cdlemk37  41170  cdlemky  41182  cdlemk11ta  41185  cdlemkid3N  41189  cdlemk11tc  41201  cdlemk11t  41202  cdlemk45  41203  cdlemk46  41204  cdlemk47  41205  cdlemk48  41206  cdlemk49  41207  cdlemk50  41208  cdlemk51  41209  cdlemk52  41210  cdlemk55b  41216  cdlemkyyN  41218  cdlemk55u1  41221  cdlemk55u  41222  cdlemk39u1  41223  cdlemk39u  41224  cdlemk56  41227  cdleml3N  41234  cdleml4N  41235  cdlemm10N  41374  dihord1  41474  dihord2a  41475  dihord2b  41476  dihord10  41479  dihord11c  41480  dihord2pre  41481  dihord4  41514  dihord5apre  41518  dihmeetlem1N  41546  dihglbcpreN  41556  dihjatc1  41567  dihjatc3  41569  dihmeetlem13N  41575  dihmeetlem20N  41582  baerlem3lem2  41966  baerlem5alem2  41967  baerlem5blem2  41968  hdmap14lem11  42134  hdmap14lem12  42135  flt4lem5  42889  monotuz  43179  congmul  43205  congsub  43208  rpnnen3lem  43269  ntrclsiso  44304  ntrclskb  44306  ntrclsk3  44307  wessf1ornlem  45425  infleinf  45612  lincdifsn  48666  itsclc0yqe  49003  itsclc0xyqsolr  49011  iscnrm3rlem8  49188  iscnrm3llem2  49191