Theorem simp11 1201

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 1087

This theorem is referenced by:  simp111  1300  simp211  1309  simp311  1318  omeulem1  8603  omeu  8606  ackbij1lem16  10259  coprimeprodsq  16777  pythagtriplem14  16797  pythagtrip  16803  mrelatglb  18552  subglsm  19628  lsmpropd  19632  mdetmul  22538  decpmatid  22685  isfil2  23773  filuni  23802  cxple2a  26646  isosctr  26766  nolesgn2o  27617  nolesgn2ores  27618  nogesgn1o  27619  nogesgn1ores  27620  nolt02o  27641  nogt01o  27642  sslttr  27753  cofcut2  27855  brbtwn2  28729  colinearalg  28734  ax5seglem3  28755  clwwlknonex2  29932  measres  33841  bayesth  34059  ofscom  35603  btwndiff  35623  ifscgr  35640  brofs2  35673  brifs2  35674  fscgr  35676  btwnconn1lem1  35683  btwnconn1lem2  35684  btwnconn1lem3  35685  btwnconn1lem4  35686  btwnconn1lem5  35687  btwnconn1lem6  35688  btwnconn1lem7  35689  btwnconn1lem8  35690  btwnconn1lem9  35691  btwnconn1lem10  35692  btwnconn1lem11  35693  btwnconn1lem12  35694  seglecgr12im  35706  seglecgr12  35707  ivthALT  35819  eqlkr  38571  lkrshp  38577  lshpkrlem5  38586  cvrval3  38886  4noncolr3  38926  4noncolr2  38927  4noncolr1  38928  athgt  38929  3dimlem2  38932  3dimlem3a  38933  3dimlem4a  38936  3dimlem4  38937  3dimlem4OLDN  38938  3dim2  38941  1cvratex  38946  hlatexch4  38954  ps-2b  38955  3atlem1  38956  3atlem2  38957  3atlem4  38959  3atlem5  38960  3atlem6  38961  llnnleat  38986  2atm  39000  ps-2c  39001  llnmlplnN  39012  lplnnlelln  39016  2atmat  39034  2llnjN  39040  lvoli2  39054  lvolnlelln  39057  4atlem3b  39071  4atlem9  39076  4atlem10a  39077  4atlem10  39079  4atlem11a  39080  4atlem11b  39081  4atlem12a  39083  4atlem12b  39084  4at  39086  4at2  39087  lplncvrlvol2  39088  2lplnj  39093  dalemswapyz  39129  dath2  39210  lneq2at  39251  2lnat  39257  cdlema1N  39264  cdlemb  39267  paddasslem15  39307  pmodlem1  39319  llnmod2i2  39336  llnexchb2lem  39341  llnexchb2  39342  dalawlem1  39344  dalawlem3  39346  dalawlem4  39347  dalawlem5  39348  dalawlem6  39349  dalawlem7  39350  dalawlem8  39351  dalawlem9  39352  dalawlem10  39353  dalawlem11  39354  dalawlem12  39355  dalawlem13  39356  dalawlem15  39358  dalaw  39359  osumcllem5N  39433  osumcllem6N  39434  osumcllem7N  39435  osumcllem9N  39437  osumcllem10N  39438  osumcllem11N  39439  pl42lem1N  39452  lhpexle3lem  39484  lhpmcvr5N  39500  lhp2atne  39507  lhp2at0ne  39509  4atexlemswapqr  39536  4atexlemex6  39547  ldilco  39589  ltrneq  39622  trlval2  39636  trlnidat  39646  cdlemd2  39672  cdlemd7  39677  cdlemd8  39678  cdleme7aa  39715  cdleme7c  39718  cdleme7d  39719  cdleme7e  39720  cdleme7ga  39721  cdleme7  39722  cdleme11c  39734  cdleme11e  39736  cdleme11l  39742  cdleme11  39743  cdleme14  39746  cdleme15a  39747  cdleme15c  39749  cdleme16b  39752  cdleme16c  39753  cdleme16d  39754  cdleme16e  39755  cdleme16f  39756  cdleme0nex  39763  cdleme18d  39768  cdleme19b  39777  cdleme19d  39779  cdleme19e  39780  cdleme20f  39787  cdleme20i  39790  cdleme20k  39792  cdleme20l1  39793  cdleme20l2  39794  cdleme20l  39795  cdleme20m  39796  cdleme21a  39798  cdleme21b  39799  cdleme21ct  39802  cdleme21d  39803  cdleme21e  39804  cdleme21f  39805  cdleme21h  39807  cdleme22eALTN  39818  cdleme22f2  39820  cdleme22g  39821  cdleme26e  39832  cdleme26eALTN  39834  cdleme26fALTN  39835  cdleme26f  39836  cdleme26f2ALTN  39837  cdleme26f2  39838  cdleme28a  39843  cdleme28b  39844  cdleme28  39846  cdleme29ex  39847  cdleme29c  39849  cdlemefrs29cpre1  39871  cdlemefr29exN  39875  cdlemefr32sn2aw  39877  cdlemefr29bpre0N  39879  cdlemefr29clN  39880  cdlemefr32fvaN  39882  cdlemefr32fva1  39883  cdlemefs32sn1aw  39887  cdleme43fsv1snlem  39893  cdleme41sn3a  39906  cdleme32fva  39910  cdleme32b  39915  cdleme32d  39917  cdleme32e  39918  cdleme32f  39919  cdleme32le  39920  cdleme35a  39921  cdleme35fnpq  39922  cdleme35b  39923  cdleme35c  39924  cdleme35d  39925  cdleme35e  39926  cdleme35f  39927  cdleme36a  39933  cdleme36m  39934  cdleme37m  39935  cdleme39a  39938  cdleme39n  39939  cdleme40m  39940  cdleme40n  39941  cdleme42e  39952  cdleme42f  39953  cdleme42g  39954  cdleme43bN  39963  cdleme43cN  39964  cdleme43dN  39965  cdleme46f2g2  39966  cdleme46f2g1  39967  cdleme17d2  39968  cdleme48b  39976  cdleme4gfv  39980  cdlemeg49le  39984  cdlemeg46c  39986  cdlemeg46fvaw  39989  cdlemeg46nlpq  39990  cdlemeg46frv  39998  cdlemeg46rgv  40001  cdlemeg46req  40002  cdlemeg46gfre  40005  cdleme50trn1  40022  cdleme50trn2a  40023  cdleme50trn2  40024  cdleme  40033  cdlemf  40036  trlord  40042  cdlemg2ce  40065  cdlemg7fvbwN  40080  cdlemg7aN  40098  cdlemg10bALTN  40109  cdlemg10a  40113  cdlemg10  40114  cdlemg12d  40119  cdlemg12f  40121  cdlemg12g  40122  cdlemg12  40123  cdlemg13a  40124  cdlemg13  40125  cdlemg17b  40135  cdlemg17dN  40136  cdlemg17dALTN  40137  cdlemg17e  40138  cdlemg17f  40139  cdlemg17g  40140  cdlemg17h  40141  cdlemg17i  40142  cdlemg17pq  40145  cdlemg17bq  40146  cdlemg17iqN  40147  cdlemg17  40150  cdlemg18d  40154  cdlemg18  40155  cdlemg19a  40156  cdlemg19  40157  cdlemg21  40159  cdlemg27a  40165  cdlemg28a  40166  cdlemg31b0N  40167  cdlemg27b  40169  cdlemg33b0  40174  cdlemg28b  40176  cdlemg28  40177  cdlemg33a  40179  cdlemg33  40184  cdlemg34  40185  cdlemg35  40186  cdlemg36  40187  ltrnco  40192  trlcone  40201  cdlemg44  40206  cdlemg47  40209  cdlemg48  40210  tendococl  40245  tendoplcl  40254  cdlemh1  40288  cdlemi  40293  cdlemj1  40294  cdlemj2  40295  tendocan  40297  cdlemk6  40310  cdlemki  40314  cdlemksat  40319  cdlemksv2  40320  cdlemk7  40321  cdlemk11  40322  cdlemk12  40323  cdlemkoatnle  40324  cdlemkole  40326  cdlemk14  40327  cdlemk15  40328  cdlemk16a  40329  cdlemk16  40330  cdlemk17  40331  cdlemk1u  40332  cdlemk5u  40334  cdlemk6u  40335  cdlemkuat  40339  cdlemk18  40341  cdlemk19  40342  cdlemk12u  40345  cdlemk21N  40346  cdlemk20  40347  cdlemkoatnle-2N  40348  cdlemk13-2N  40349  cdlemkole-2N  40350  cdlemk14-2N  40351  cdlemk15-2N  40352  cdlemk16-2N  40353  cdlemk17-2N  40354  cdlemk18-2N  40359  cdlemk19-2N  40360  cdlemk7u-2N  40361  cdlemk11u-2N  40362  cdlemk12u-2N  40363  cdlemk21-2N  40364  cdlemk20-2N  40365  cdlemk22  40366  cdlemk23-3  40375  cdlemk25-3  40377  cdlemk26b-3  40378  cdlemk27-3  40380  cdlemk28-3  40381  cdlemk33N  40382  cdlemk37  40387  cdlemky  40399  cdlemk11ta  40402  cdlemkid3N  40406  cdlemk11tc  40418  cdlemk11t  40419  cdlemk45  40420  cdlemk46  40421  cdlemk47  40422  cdlemk48  40423  cdlemk49  40424  cdlemk50  40425  cdlemk51  40426  cdlemk52  40427  cdlemk55b  40433  cdlemkyyN  40435  cdlemk55u1  40438  cdlemk55u  40439  cdlemk39u1  40440  cdlemk39u  40441  cdlemk56  40444  cdleml3N  40451  cdleml4N  40452  cdlemm10N  40591  dihord1  40691  dihord2a  40692  dihord2b  40693  dihord10  40696  dihord11c  40697  dihord2pre  40698  dihord4  40731  dihord5apre  40735  dihmeetlem1N  40763  dihglbcpreN  40773  dihjatc1  40784  dihjatc3  40786  dihmeetlem13N  40792  dihmeetlem20N  40799  baerlem3lem2  41183  baerlem5alem2  41184  baerlem5blem2  41185  hdmap14lem11  41351  hdmap14lem12  41352  flt4lem5  42074  monotuz  42362  congmul  42388  congsub  42391  rpnnen3lem  42452  ntrclsiso  43497  ntrclskb  43499  ntrclsk3  43500  wessf1ornlem  44558  infleinf  44754  lincdifsn  47492  itsclc0yqe  47834  itsclc0xyqsolr  47842  iscnrm3rlem8  47966  iscnrm3llem2  47969