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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simp111  1302  simp211  1311  simp311  1320  omeulem1  8581  omeu  8584  ackbij1lem16  10229  coprimeprodsq  16740  pythagtriplem14  16760  pythagtrip  16766  mrelatglb  18512  subglsm  19540  lsmpropd  19544  mdetmul  22124  decpmatid  22271  isfil2  23359  filuni  23388  cxple2a  26206  isosctr  26323  nolesgn2o  27171  nolesgn2ores  27172  nogesgn1o  27173  nogesgn1ores  27174  nolt02o  27195  nogt01o  27196  sslttr  27305  cofcut2  27406  brbtwn2  28160  colinearalg  28165  ax5seglem3  28186  clwwlknonex2  29359  measres  33215  bayesth  33433  ofscom  34974  btwndiff  34994  ifscgr  35011  brofs2  35044  brifs2  35045  fscgr  35047  btwnconn1lem1  35054  btwnconn1lem2  35055  btwnconn1lem3  35056  btwnconn1lem4  35057  btwnconn1lem5  35058  btwnconn1lem6  35059  btwnconn1lem7  35060  btwnconn1lem8  35061  btwnconn1lem9  35062  btwnconn1lem10  35063  btwnconn1lem11  35064  btwnconn1lem12  35065  seglecgr12im  35077  seglecgr12  35078  ivthALT  35215  eqlkr  37964  lkrshp  37970  lshpkrlem5  37979  cvrval3  38279  4noncolr3  38319  4noncolr2  38320  4noncolr1  38321  athgt  38322  3dimlem2  38325  3dimlem3a  38326  3dimlem4a  38329  3dimlem4  38330  3dimlem4OLDN  38331  3dim2  38334  1cvratex  38339  hlatexch4  38347  ps-2b  38348  3atlem1  38349  3atlem2  38350  3atlem4  38352  3atlem5  38353  3atlem6  38354  llnnleat  38379  2atm  38393  ps-2c  38394  llnmlplnN  38405  lplnnlelln  38409  2atmat  38427  2llnjN  38433  lvoli2  38447  lvolnlelln  38450  4atlem3b  38464  4atlem9  38469  4atlem10a  38470  4atlem10  38472  4atlem11a  38473  4atlem11b  38474  4atlem12a  38476  4atlem12b  38477  4at  38479  4at2  38480  lplncvrlvol2  38481  2lplnj  38486  dalemswapyz  38522  dath2  38603  lneq2at  38644  2lnat  38650  cdlema1N  38657  cdlemb  38660  paddasslem15  38700  pmodlem1  38712  llnmod2i2  38729  llnexchb2lem  38734  llnexchb2  38735  dalawlem1  38737  dalawlem3  38739  dalawlem4  38740  dalawlem5  38741  dalawlem6  38742  dalawlem7  38743  dalawlem8  38744  dalawlem9  38745  dalawlem10  38746  dalawlem11  38747  dalawlem12  38748  dalawlem13  38749  dalawlem15  38751  dalaw  38752  osumcllem5N  38826  osumcllem6N  38827  osumcllem7N  38828  osumcllem9N  38830  osumcllem10N  38831  osumcllem11N  38832  pl42lem1N  38845  lhpexle3lem  38877  lhpmcvr5N  38893  lhp2atne  38900  lhp2at0ne  38902  4atexlemswapqr  38929  4atexlemex6  38940  ldilco  38982  ltrneq  39015  trlval2  39029  trlnidat  39039  cdlemd2  39065  cdlemd7  39070  cdlemd8  39071  cdleme7aa  39108  cdleme7c  39111  cdleme7d  39112  cdleme7e  39113  cdleme7ga  39114  cdleme7  39115  cdleme11c  39127  cdleme11e  39129  cdleme11l  39135  cdleme11  39136  cdleme14  39139  cdleme15a  39140  cdleme15c  39142  cdleme16b  39145  cdleme16c  39146  cdleme16d  39147  cdleme16e  39148  cdleme16f  39149  cdleme0nex  39156  cdleme18d  39161  cdleme19b  39170  cdleme19d  39172  cdleme19e  39173  cdleme20f  39180  cdleme20i  39183  cdleme20k  39185  cdleme20l1  39186  cdleme20l2  39187  cdleme20l  39188  cdleme20m  39189  cdleme21a  39191  cdleme21b  39192  cdleme21ct  39195  cdleme21d  39196  cdleme21e  39197  cdleme21f  39198  cdleme21h  39200  cdleme22eALTN  39211  cdleme22f2  39213  cdleme22g  39214  cdleme26e  39225  cdleme26eALTN  39227  cdleme26fALTN  39228  cdleme26f  39229  cdleme26f2ALTN  39230  cdleme26f2  39231  cdleme28a  39236  cdleme28b  39237  cdleme28  39239  cdleme29ex  39240  cdleme29c  39242  cdlemefrs29cpre1  39264  cdlemefr29exN  39268  cdlemefr32sn2aw  39270  cdlemefr29bpre0N  39272  cdlemefr29clN  39273  cdlemefr32fvaN  39275  cdlemefr32fva1  39276  cdlemefs32sn1aw  39280  cdleme43fsv1snlem  39286  cdleme41sn3a  39299  cdleme32fva  39303  cdleme32b  39308  cdleme32d  39310  cdleme32e  39311  cdleme32f  39312  cdleme32le  39313  cdleme35a  39314  cdleme35fnpq  39315  cdleme35b  39316  cdleme35c  39317  cdleme35d  39318  cdleme35e  39319  cdleme35f  39320  cdleme36a  39326  cdleme36m  39327  cdleme37m  39328  cdleme39a  39331  cdleme39n  39332  cdleme40m  39333  cdleme40n  39334  cdleme42e  39345  cdleme42f  39346  cdleme42g  39347  cdleme43bN  39356  cdleme43cN  39357  cdleme43dN  39358  cdleme46f2g2  39359  cdleme46f2g1  39360  cdleme17d2  39361  cdleme48b  39369  cdleme4gfv  39373  cdlemeg49le  39377  cdlemeg46c  39379  cdlemeg46fvaw  39382  cdlemeg46nlpq  39383  cdlemeg46frv  39391  cdlemeg46rgv  39394  cdlemeg46req  39395  cdlemeg46gfre  39398  cdleme50trn1  39415  cdleme50trn2a  39416  cdleme50trn2  39417  cdleme  39426  cdlemf  39429  trlord  39435  cdlemg2ce  39458  cdlemg7fvbwN  39473  cdlemg7aN  39491  cdlemg10bALTN  39502  cdlemg10a  39506  cdlemg10  39507  cdlemg12d  39512  cdlemg12f  39514  cdlemg12g  39515  cdlemg12  39516  cdlemg13a  39517  cdlemg13  39518  cdlemg17b  39528  cdlemg17dN  39529  cdlemg17dALTN  39530  cdlemg17e  39531  cdlemg17f  39532  cdlemg17g  39533  cdlemg17h  39534  cdlemg17i  39535  cdlemg17pq  39538  cdlemg17bq  39539  cdlemg17iqN  39540  cdlemg17  39543  cdlemg18d  39547  cdlemg18  39548  cdlemg19a  39549  cdlemg19  39550  cdlemg21  39552  cdlemg27a  39558  cdlemg28a  39559  cdlemg31b0N  39560  cdlemg27b  39562  cdlemg33b0  39567  cdlemg28b  39569  cdlemg28  39570  cdlemg33a  39572  cdlemg33  39577  cdlemg34  39578  cdlemg35  39579  cdlemg36  39580  ltrnco  39585  trlcone  39594  cdlemg44  39599  cdlemg47  39602  cdlemg48  39603  tendococl  39638  tendoplcl  39647  cdlemh1  39681  cdlemi  39686  cdlemj1  39687  cdlemj2  39688  tendocan  39690  cdlemk6  39703  cdlemki  39707  cdlemksat  39712  cdlemksv2  39713  cdlemk7  39714  cdlemk11  39715  cdlemk12  39716  cdlemkoatnle  39717  cdlemkole  39719  cdlemk14  39720  cdlemk15  39721  cdlemk16a  39722  cdlemk16  39723  cdlemk17  39724  cdlemk1u  39725  cdlemk5u  39727  cdlemk6u  39728  cdlemkuat  39732  cdlemk18  39734  cdlemk19  39735  cdlemk12u  39738  cdlemk21N  39739  cdlemk20  39740  cdlemkoatnle-2N  39741  cdlemk13-2N  39742  cdlemkole-2N  39743  cdlemk14-2N  39744  cdlemk15-2N  39745  cdlemk16-2N  39746  cdlemk17-2N  39747  cdlemk18-2N  39752  cdlemk19-2N  39753  cdlemk7u-2N  39754  cdlemk11u-2N  39755  cdlemk12u-2N  39756  cdlemk21-2N  39757  cdlemk20-2N  39758  cdlemk22  39759  cdlemk23-3  39768  cdlemk25-3  39770  cdlemk26b-3  39771  cdlemk27-3  39773  cdlemk28-3  39774  cdlemk33N  39775  cdlemk37  39780  cdlemky  39792  cdlemk11ta  39795  cdlemkid3N  39799  cdlemk11tc  39811  cdlemk11t  39812  cdlemk45  39813  cdlemk46  39814  cdlemk47  39815  cdlemk48  39816  cdlemk49  39817  cdlemk50  39818  cdlemk51  39819  cdlemk52  39820  cdlemk55b  39826  cdlemkyyN  39828  cdlemk55u1  39831  cdlemk55u  39832  cdlemk39u1  39833  cdlemk39u  39834  cdlemk56  39837  cdleml3N  39844  cdleml4N  39845  cdlemm10N  39984  dihord1  40084  dihord2a  40085  dihord2b  40086  dihord10  40089  dihord11c  40090  dihord2pre  40091  dihord4  40124  dihord5apre  40128  dihmeetlem1N  40156  dihglbcpreN  40166  dihjatc1  40177  dihjatc3  40179  dihmeetlem13N  40185  dihmeetlem20N  40192  baerlem3lem2  40576  baerlem5alem2  40577  baerlem5blem2  40578  hdmap14lem11  40744  hdmap14lem12  40745  flt4lem5  41393  monotuz  41670  congmul  41696  congsub  41699  rpnnen3lem  41760  ntrclsiso  42808  ntrclskb  42810  ntrclsk3  42811  wessf1ornlem  43872  infleinf  44072  lincdifsn  47095  itsclc0yqe  47437  itsclc0xyqsolr  47445  iscnrm3rlem8  47570  iscnrm3llem2  47573