Theorem simp11 1203

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 1087

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 1089

This theorem is referenced by:  simp111  1302  simp211  1311  simp311  1320  omeulem1  8638  omeu  8641  ackbij1lem16  10303  coprimeprodsq  16855  pythagtriplem14  16875  pythagtrip  16881  mrelatglb  18630  subglsm  19715  lsmpropd  19719  mdetmul  22650  decpmatid  22797  isfil2  23885  filuni  23914  cxple2a  26759  isosctr  26882  nolesgn2o  27734  nolesgn2ores  27735  nogesgn1o  27736  nogesgn1ores  27737  nolt02o  27758  nogt01o  27759  sslttr  27870  cofcut2  27974  brbtwn2  28938  colinearalg  28943  ax5seglem3  28964  clwwlknonex2  30141  measres  34186  bayesth  34404  ofscom  35971  btwndiff  35991  ifscgr  36008  brofs2  36041  brifs2  36042  fscgr  36044  btwnconn1lem1  36051  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem7  36057  btwnconn1lem8  36058  btwnconn1lem9  36059  btwnconn1lem10  36060  btwnconn1lem11  36061  btwnconn1lem12  36062  seglecgr12im  36074  seglecgr12  36075  ivthALT  36301  eqlkr  39055  lkrshp  39061  lshpkrlem5  39070  cvrval3  39370  4noncolr3  39410  4noncolr2  39411  4noncolr1  39412  athgt  39413  3dimlem2  39416  3dimlem3a  39417  3dimlem4a  39420  3dimlem4  39421  3dimlem4OLDN  39422  3dim2  39425  1cvratex  39430  hlatexch4  39438  ps-2b  39439  3atlem1  39440  3atlem2  39441  3atlem4  39443  3atlem5  39444  3atlem6  39445  llnnleat  39470  2atm  39484  ps-2c  39485  llnmlplnN  39496  lplnnlelln  39500  2atmat  39518  2llnjN  39524  lvoli2  39538  lvolnlelln  39541  4atlem3b  39555  4atlem9  39560  4atlem10a  39561  4atlem10  39563  4atlem11a  39564  4atlem11b  39565  4atlem12a  39567  4atlem12b  39568  4at  39570  4at2  39571  lplncvrlvol2  39572  2lplnj  39577  dalemswapyz  39613  dath2  39694  lneq2at  39735  2lnat  39741  cdlema1N  39748  cdlemb  39751  paddasslem15  39791  pmodlem1  39803  llnmod2i2  39820  llnexchb2lem  39825  llnexchb2  39826  dalawlem1  39828  dalawlem3  39830  dalawlem4  39831  dalawlem5  39832  dalawlem6  39833  dalawlem7  39834  dalawlem8  39835  dalawlem9  39836  dalawlem10  39837  dalawlem11  39838  dalawlem12  39839  dalawlem13  39840  dalawlem15  39842  dalaw  39843  osumcllem5N  39917  osumcllem6N  39918  osumcllem7N  39919  osumcllem9N  39921  osumcllem10N  39922  osumcllem11N  39923  pl42lem1N  39936  lhpexle3lem  39968  lhpmcvr5N  39984  lhp2atne  39991  lhp2at0ne  39993  4atexlemswapqr  40020  4atexlemex6  40031  ldilco  40073  ltrneq  40106  trlval2  40120  trlnidat  40130  cdlemd2  40156  cdlemd7  40161  cdlemd8  40162  cdleme7aa  40199  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme11c  40218  cdleme11e  40220  cdleme11l  40226  cdleme11  40227  cdleme14  40230  cdleme15a  40231  cdleme15c  40233  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme16e  40239  cdleme16f  40240  cdleme0nex  40247  cdleme18d  40252  cdleme19b  40261  cdleme19d  40263  cdleme19e  40264  cdleme20f  40271  cdleme20i  40274  cdleme20k  40276  cdleme20l1  40277  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme21a  40282  cdleme21b  40283  cdleme21ct  40286  cdleme21d  40287  cdleme21e  40288  cdleme21f  40289  cdleme21h  40291  cdleme22eALTN  40302  cdleme22f2  40304  cdleme22g  40305  cdleme26e  40316  cdleme26eALTN  40318  cdleme26fALTN  40319  cdleme26f  40320  cdleme26f2ALTN  40321  cdleme26f2  40322  cdleme28a  40327  cdleme28b  40328  cdleme28  40330  cdleme29ex  40331  cdleme29c  40333  cdlemefrs29cpre1  40355  cdlemefr29exN  40359  cdlemefr32sn2aw  40361  cdlemefr29bpre0N  40363  cdlemefr29clN  40364  cdlemefr32fvaN  40366  cdlemefr32fva1  40367  cdlemefs32sn1aw  40371  cdleme43fsv1snlem  40377  cdleme41sn3a  40390  cdleme32fva  40394  cdleme32b  40399  cdleme32d  40401  cdleme32e  40402  cdleme32f  40403  cdleme32le  40404  cdleme35a  40405  cdleme35fnpq  40406  cdleme35b  40407  cdleme35c  40408  cdleme35d  40409  cdleme35e  40410  cdleme35f  40411  cdleme36a  40417  cdleme36m  40418  cdleme37m  40419  cdleme39a  40422  cdleme39n  40423  cdleme40m  40424  cdleme40n  40425  cdleme42e  40436  cdleme42f  40437  cdleme42g  40438  cdleme43bN  40447  cdleme43cN  40448  cdleme43dN  40449  cdleme46f2g2  40450  cdleme46f2g1  40451  cdleme17d2  40452  cdleme48b  40460  cdleme4gfv  40464  cdlemeg49le  40468  cdlemeg46c  40470  cdlemeg46fvaw  40473  cdlemeg46nlpq  40474  cdlemeg46frv  40482  cdlemeg46rgv  40485  cdlemeg46req  40486  cdlemeg46gfre  40489  cdleme50trn1  40506  cdleme50trn2a  40507  cdleme50trn2  40508  cdleme  40517  cdlemf  40520  trlord  40526  cdlemg2ce  40549  cdlemg7fvbwN  40564  cdlemg7aN  40582  cdlemg10bALTN  40593  cdlemg10a  40597  cdlemg10  40598  cdlemg12d  40603  cdlemg12f  40605  cdlemg12g  40606  cdlemg12  40607  cdlemg13a  40608  cdlemg13  40609  cdlemg17b  40619  cdlemg17dN  40620  cdlemg17dALTN  40621  cdlemg17e  40622  cdlemg17f  40623  cdlemg17g  40624  cdlemg17h  40625  cdlemg17i  40626  cdlemg17pq  40629  cdlemg17bq  40630  cdlemg17iqN  40631  cdlemg17  40634  cdlemg18d  40638  cdlemg18  40639  cdlemg19a  40640  cdlemg19  40641  cdlemg21  40643  cdlemg27a  40649  cdlemg28a  40650  cdlemg31b0N  40651  cdlemg27b  40653  cdlemg33b0  40658  cdlemg28b  40660  cdlemg28  40661  cdlemg33a  40663  cdlemg33  40668  cdlemg34  40669  cdlemg35  40670  cdlemg36  40671  ltrnco  40676  trlcone  40685  cdlemg44  40690  cdlemg47  40693  cdlemg48  40694  tendococl  40729  tendoplcl  40738  cdlemh1  40772  cdlemi  40777  cdlemj1  40778  cdlemj2  40779  tendocan  40781  cdlemk6  40794  cdlemki  40798  cdlemksat  40803  cdlemksv2  40804  cdlemk7  40805  cdlemk11  40806  cdlemk12  40807  cdlemkoatnle  40808  cdlemkole  40810  cdlemk14  40811  cdlemk15  40812  cdlemk16a  40813  cdlemk16  40814  cdlemk17  40815  cdlemk1u  40816  cdlemk5u  40818  cdlemk6u  40819  cdlemkuat  40823  cdlemk18  40825  cdlemk19  40826  cdlemk12u  40829  cdlemk21N  40830  cdlemk20  40831  cdlemkoatnle-2N  40832  cdlemk13-2N  40833  cdlemkole-2N  40834  cdlemk14-2N  40835  cdlemk15-2N  40836  cdlemk16-2N  40837  cdlemk17-2N  40838  cdlemk18-2N  40843  cdlemk19-2N  40844  cdlemk7u-2N  40845  cdlemk11u-2N  40846  cdlemk12u-2N  40847  cdlemk21-2N  40848  cdlemk20-2N  40849  cdlemk22  40850  cdlemk23-3  40859  cdlemk25-3  40861  cdlemk26b-3  40862  cdlemk27-3  40864  cdlemk28-3  40865  cdlemk33N  40866  cdlemk37  40871  cdlemky  40883  cdlemk11ta  40886  cdlemkid3N  40890  cdlemk11tc  40902  cdlemk11t  40903  cdlemk45  40904  cdlemk46  40905  cdlemk47  40906  cdlemk48  40907  cdlemk49  40908  cdlemk50  40909  cdlemk51  40910  cdlemk52  40911  cdlemk55b  40917  cdlemkyyN  40919  cdlemk55u1  40922  cdlemk55u  40923  cdlemk39u1  40924  cdlemk39u  40925  cdlemk56  40928  cdleml3N  40935  cdleml4N  40936  cdlemm10N  41075  dihord1  41175  dihord2a  41176  dihord2b  41177  dihord10  41180  dihord11c  41181  dihord2pre  41182  dihord4  41215  dihord5apre  41219  dihmeetlem1N  41247  dihglbcpreN  41257  dihjatc1  41268  dihjatc3  41270  dihmeetlem13N  41276  dihmeetlem20N  41283  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  hdmap14lem11  41835  hdmap14lem12  41836  flt4lem5  42605  monotuz  42898  congmul  42924  congsub  42927  rpnnen3lem  42988  ntrclsiso  44029  ntrclskb  44031  ntrclsk3  44032  wessf1ornlem  45092  infleinf  45287  lincdifsn  48153  itsclc0yqe  48495  itsclc0xyqsolr  48503  iscnrm3rlem8  48627  iscnrm3llem2  48630