Theorem simp11 1200

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 1133	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	3ad2ant1 1130	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  simp111  1299  simp211  1308  simp311  1317  omeulem1  8578  omeu  8581  ackbij1lem16  10227  coprimeprodsq  16746  pythagtriplem14  16766  pythagtrip  16772  mrelatglb  18521  subglsm  19589  lsmpropd  19593  mdetmul  22469  decpmatid  22616  isfil2  23704  filuni  23733  cxple2a  26574  isosctr  26694  nolesgn2o  27545  nolesgn2ores  27546  nogesgn1o  27547  nogesgn1ores  27548  nolt02o  27569  nogt01o  27570  sslttr  27681  cofcut2  27783  brbtwn2  28657  colinearalg  28662  ax5seglem3  28683  clwwlknonex2  29857  measres  33740  bayesth  33958  ofscom  35502  btwndiff  35522  ifscgr  35539  brofs2  35572  brifs2  35573  fscgr  35575  btwnconn1lem1  35582  btwnconn1lem2  35583  btwnconn1lem3  35584  btwnconn1lem4  35585  btwnconn1lem5  35586  btwnconn1lem6  35587  btwnconn1lem7  35588  btwnconn1lem8  35589  btwnconn1lem9  35590  btwnconn1lem10  35591  btwnconn1lem11  35592  btwnconn1lem12  35593  seglecgr12im  35605  seglecgr12  35606  ivthALT  35721  eqlkr  38473  lkrshp  38479  lshpkrlem5  38488  cvrval3  38788  4noncolr3  38828  4noncolr2  38829  4noncolr1  38830  athgt  38831  3dimlem2  38834  3dimlem3a  38835  3dimlem4a  38838  3dimlem4  38839  3dimlem4OLDN  38840  3dim2  38843  1cvratex  38848  hlatexch4  38856  ps-2b  38857  3atlem1  38858  3atlem2  38859  3atlem4  38861  3atlem5  38862  3atlem6  38863  llnnleat  38888  2atm  38902  ps-2c  38903  llnmlplnN  38914  lplnnlelln  38918  2atmat  38936  2llnjN  38942  lvoli2  38956  lvolnlelln  38959  4atlem3b  38973  4atlem9  38978  4atlem10a  38979  4atlem10  38981  4atlem11a  38982  4atlem11b  38983  4atlem12a  38985  4atlem12b  38986  4at  38988  4at2  38989  lplncvrlvol2  38990  2lplnj  38995  dalemswapyz  39031  dath2  39112  lneq2at  39153  2lnat  39159  cdlema1N  39166  cdlemb  39169  paddasslem15  39209  pmodlem1  39221  llnmod2i2  39238  llnexchb2lem  39243  llnexchb2  39244  dalawlem1  39246  dalawlem3  39248  dalawlem4  39249  dalawlem5  39250  dalawlem6  39251  dalawlem7  39252  dalawlem8  39253  dalawlem9  39254  dalawlem10  39255  dalawlem11  39256  dalawlem12  39257  dalawlem13  39258  dalawlem15  39260  dalaw  39261  osumcllem5N  39335  osumcllem6N  39336  osumcllem7N  39337  osumcllem9N  39339  osumcllem10N  39340  osumcllem11N  39341  pl42lem1N  39354  lhpexle3lem  39386  lhpmcvr5N  39402  lhp2atne  39409  lhp2at0ne  39411  4atexlemswapqr  39438  4atexlemex6  39449  ldilco  39491  ltrneq  39524  trlval2  39538  trlnidat  39548  cdlemd2  39574  cdlemd7  39579  cdlemd8  39580  cdleme7aa  39617  cdleme7c  39620  cdleme7d  39621  cdleme7e  39622  cdleme7ga  39623  cdleme7  39624  cdleme11c  39636  cdleme11e  39638  cdleme11l  39644  cdleme11  39645  cdleme14  39648  cdleme15a  39649  cdleme15c  39651  cdleme16b  39654  cdleme16c  39655  cdleme16d  39656  cdleme16e  39657  cdleme16f  39658  cdleme0nex  39665  cdleme18d  39670  cdleme19b  39679  cdleme19d  39681  cdleme19e  39682  cdleme20f  39689  cdleme20i  39692  cdleme20k  39694  cdleme20l1  39695  cdleme20l2  39696  cdleme20l  39697  cdleme20m  39698  cdleme21a  39700  cdleme21b  39701  cdleme21ct  39704  cdleme21d  39705  cdleme21e  39706  cdleme21f  39707  cdleme21h  39709  cdleme22eALTN  39720  cdleme22f2  39722  cdleme22g  39723  cdleme26e  39734  cdleme26eALTN  39736  cdleme26fALTN  39737  cdleme26f  39738  cdleme26f2ALTN  39739  cdleme26f2  39740  cdleme28a  39745  cdleme28b  39746  cdleme28  39748  cdleme29ex  39749  cdleme29c  39751  cdlemefrs29cpre1  39773  cdlemefr29exN  39777  cdlemefr32sn2aw  39779  cdlemefr29bpre0N  39781  cdlemefr29clN  39782  cdlemefr32fvaN  39784  cdlemefr32fva1  39785  cdlemefs32sn1aw  39789  cdleme43fsv1snlem  39795  cdleme41sn3a  39808  cdleme32fva  39812  cdleme32b  39817  cdleme32d  39819  cdleme32e  39820  cdleme32f  39821  cdleme32le  39822  cdleme35a  39823  cdleme35fnpq  39824  cdleme35b  39825  cdleme35c  39826  cdleme35d  39827  cdleme35e  39828  cdleme35f  39829  cdleme36a  39835  cdleme36m  39836  cdleme37m  39837  cdleme39a  39840  cdleme39n  39841  cdleme40m  39842  cdleme40n  39843  cdleme42e  39854  cdleme42f  39855  cdleme42g  39856  cdleme43bN  39865  cdleme43cN  39866  cdleme43dN  39867  cdleme46f2g2  39868  cdleme46f2g1  39869  cdleme17d2  39870  cdleme48b  39878  cdleme4gfv  39882  cdlemeg49le  39886  cdlemeg46c  39888  cdlemeg46fvaw  39891  cdlemeg46nlpq  39892  cdlemeg46frv  39900  cdlemeg46rgv  39903  cdlemeg46req  39904  cdlemeg46gfre  39907  cdleme50trn1  39924  cdleme50trn2a  39925  cdleme50trn2  39926  cdleme  39935  cdlemf  39938  trlord  39944  cdlemg2ce  39967  cdlemg7fvbwN  39982  cdlemg7aN  40000  cdlemg10bALTN  40011  cdlemg10a  40015  cdlemg10  40016  cdlemg12d  40021  cdlemg12f  40023  cdlemg12g  40024  cdlemg12  40025  cdlemg13a  40026  cdlemg13  40027  cdlemg17b  40037  cdlemg17dN  40038  cdlemg17dALTN  40039  cdlemg17e  40040  cdlemg17f  40041  cdlemg17g  40042  cdlemg17h  40043  cdlemg17i  40044  cdlemg17pq  40047  cdlemg17bq  40048  cdlemg17iqN  40049  cdlemg17  40052  cdlemg18d  40056  cdlemg18  40057  cdlemg19a  40058  cdlemg19  40059  cdlemg21  40061  cdlemg27a  40067  cdlemg28a  40068  cdlemg31b0N  40069  cdlemg27b  40071  cdlemg33b0  40076  cdlemg28b  40078  cdlemg28  40079  cdlemg33a  40081  cdlemg33  40086  cdlemg34  40087  cdlemg35  40088  cdlemg36  40089  ltrnco  40094  trlcone  40103  cdlemg44  40108  cdlemg47  40111  cdlemg48  40112  tendococl  40147  tendoplcl  40156  cdlemh1  40190  cdlemi  40195  cdlemj1  40196  cdlemj2  40197  tendocan  40199  cdlemk6  40212  cdlemki  40216  cdlemksat  40221  cdlemksv2  40222  cdlemk7  40223  cdlemk11  40224  cdlemk12  40225  cdlemkoatnle  40226  cdlemkole  40228  cdlemk14  40229  cdlemk15  40230  cdlemk16a  40231  cdlemk16  40232  cdlemk17  40233  cdlemk1u  40234  cdlemk5u  40236  cdlemk6u  40237  cdlemkuat  40241  cdlemk18  40243  cdlemk19  40244  cdlemk12u  40247  cdlemk21N  40248  cdlemk20  40249  cdlemkoatnle-2N  40250  cdlemk13-2N  40251  cdlemkole-2N  40252  cdlemk14-2N  40253  cdlemk15-2N  40254  cdlemk16-2N  40255  cdlemk17-2N  40256  cdlemk18-2N  40261  cdlemk19-2N  40262  cdlemk7u-2N  40263  cdlemk11u-2N  40264  cdlemk12u-2N  40265  cdlemk21-2N  40266  cdlemk20-2N  40267  cdlemk22  40268  cdlemk23-3  40277  cdlemk25-3  40279  cdlemk26b-3  40280  cdlemk27-3  40282  cdlemk28-3  40283  cdlemk33N  40284  cdlemk37  40289  cdlemky  40301  cdlemk11ta  40304  cdlemkid3N  40308  cdlemk11tc  40320  cdlemk11t  40321  cdlemk45  40322  cdlemk46  40323  cdlemk47  40324  cdlemk48  40325  cdlemk49  40326  cdlemk50  40327  cdlemk51  40328  cdlemk52  40329  cdlemk55b  40335  cdlemkyyN  40337  cdlemk55u1  40340  cdlemk55u  40341  cdlemk39u1  40342  cdlemk39u  40343  cdlemk56  40346  cdleml3N  40353  cdleml4N  40354  cdlemm10N  40493  dihord1  40593  dihord2a  40594  dihord2b  40595  dihord10  40598  dihord11c  40599  dihord2pre  40600  dihord4  40633  dihord5apre  40637  dihmeetlem1N  40665  dihglbcpreN  40675  dihjatc1  40686  dihjatc3  40688  dihmeetlem13N  40694  dihmeetlem20N  40701  baerlem3lem2  41085  baerlem5alem2  41086  baerlem5blem2  41087  hdmap14lem11  41253  hdmap14lem12  41254  flt4lem5  41944  monotuz  42232  congmul  42258  congsub  42261  rpnnen3lem  42322  ntrclsiso  43368  ntrclskb  43370  ntrclsk3  43371  wessf1ornlem  44430  infleinf  44628  lincdifsn  47354  itsclc0yqe  47696  itsclc0xyqsolr  47704  iscnrm3rlem8  47828  iscnrm3llem2  47831