Theorem simp11 1202

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 1135	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	3ad2ant1 1132	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp111  1301  simp211  1310  simp311  1319  omeulem1  8422  omeu  8425  ackbij1lem16  10000  coprimeprodsq  16518  pythagtriplem14  16538  pythagtrip  16544  mrelatglb  18287  subglsm  19288  lsmpropd  19292  mdetmul  21781  decpmatid  21928  isfil2  23016  filuni  23045  cxple2a  25863  isosctr  25980  brbtwn2  27282  colinearalg  27287  ax5seglem3  27308  clwwlknonex2  28482  measres  32199  bayesth  32415  nolesgn2o  33883  nolesgn2ores  33884  nogesgn1o  33885  nogesgn1ores  33886  nolt02o  33907  nogt01o  33908  sslttr  34010  cofcut2  34100  ofscom  34318  btwndiff  34338  ifscgr  34355  brofs2  34388  brifs2  34389  fscgr  34391  btwnconn1lem1  34398  btwnconn1lem2  34399  btwnconn1lem3  34400  btwnconn1lem4  34401  btwnconn1lem5  34402  btwnconn1lem6  34403  btwnconn1lem7  34404  btwnconn1lem8  34405  btwnconn1lem9  34406  btwnconn1lem10  34407  btwnconn1lem11  34408  btwnconn1lem12  34409  seglecgr12im  34421  seglecgr12  34422  ivthALT  34533  eqlkr  37120  lkrshp  37126  lshpkrlem5  37135  cvrval3  37434  4noncolr3  37474  4noncolr2  37475  4noncolr1  37476  athgt  37477  3dimlem2  37480  3dimlem3a  37481  3dimlem4a  37484  3dimlem4  37485  3dimlem4OLDN  37486  3dim2  37489  1cvratex  37494  hlatexch4  37502  ps-2b  37503  3atlem1  37504  3atlem2  37505  3atlem4  37507  3atlem5  37508  3atlem6  37509  llnnleat  37534  2atm  37548  ps-2c  37549  llnmlplnN  37560  lplnnlelln  37564  2atmat  37582  2llnjN  37588  lvoli2  37602  lvolnlelln  37605  4atlem3b  37619  4atlem9  37624  4atlem10a  37625  4atlem10  37627  4atlem11a  37628  4atlem11b  37629  4atlem12a  37631  4atlem12b  37632  4at  37634  4at2  37635  lplncvrlvol2  37636  2lplnj  37641  dalemswapyz  37677  dath2  37758  lneq2at  37799  2lnat  37805  cdlema1N  37812  cdlemb  37815  paddasslem15  37855  pmodlem1  37867  llnmod2i2  37884  llnexchb2lem  37889  llnexchb2  37890  dalawlem1  37892  dalawlem3  37894  dalawlem4  37895  dalawlem5  37896  dalawlem6  37897  dalawlem7  37898  dalawlem8  37899  dalawlem9  37900  dalawlem10  37901  dalawlem11  37902  dalawlem12  37903  dalawlem13  37904  dalawlem15  37906  dalaw  37907  osumcllem5N  37981  osumcllem6N  37982  osumcllem7N  37983  osumcllem9N  37985  osumcllem10N  37986  osumcllem11N  37987  pl42lem1N  38000  lhpexle3lem  38032  lhpmcvr5N  38048  lhp2atne  38055  lhp2at0ne  38057  4atexlemswapqr  38084  4atexlemex6  38095  ldilco  38137  ltrneq  38170  trlval2  38184  trlnidat  38194  cdlemd2  38220  cdlemd7  38225  cdlemd8  38226  cdleme7aa  38263  cdleme7c  38266  cdleme7d  38267  cdleme7e  38268  cdleme7ga  38269  cdleme7  38270  cdleme11c  38282  cdleme11e  38284  cdleme11l  38290  cdleme11  38291  cdleme14  38294  cdleme15a  38295  cdleme15c  38297  cdleme16b  38300  cdleme16c  38301  cdleme16d  38302  cdleme16e  38303  cdleme16f  38304  cdleme0nex  38311  cdleme18d  38316  cdleme19b  38325  cdleme19d  38327  cdleme19e  38328  cdleme20f  38335  cdleme20i  38338  cdleme20k  38340  cdleme20l1  38341  cdleme20l2  38342  cdleme20l  38343  cdleme20m  38344  cdleme21a  38346  cdleme21b  38347  cdleme21ct  38350  cdleme21d  38351  cdleme21e  38352  cdleme21f  38353  cdleme21h  38355  cdleme22eALTN  38366  cdleme22f2  38368  cdleme22g  38369  cdleme26e  38380  cdleme26eALTN  38382  cdleme26fALTN  38383  cdleme26f  38384  cdleme26f2ALTN  38385  cdleme26f2  38386  cdleme28a  38391  cdleme28b  38392  cdleme28  38394  cdleme29ex  38395  cdleme29c  38397  cdlemefrs29cpre1  38419  cdlemefr29exN  38423  cdlemefr32sn2aw  38425  cdlemefr29bpre0N  38427  cdlemefr29clN  38428  cdlemefr32fvaN  38430  cdlemefr32fva1  38431  cdlemefs32sn1aw  38435  cdleme43fsv1snlem  38441  cdleme41sn3a  38454  cdleme32fva  38458  cdleme32b  38463  cdleme32d  38465  cdleme32e  38466  cdleme32f  38467  cdleme32le  38468  cdleme35a  38469  cdleme35fnpq  38470  cdleme35b  38471  cdleme35c  38472  cdleme35d  38473  cdleme35e  38474  cdleme35f  38475  cdleme36a  38481  cdleme36m  38482  cdleme37m  38483  cdleme39a  38486  cdleme39n  38487  cdleme40m  38488  cdleme40n  38489  cdleme42e  38500  cdleme42f  38501  cdleme42g  38502  cdleme43bN  38511  cdleme43cN  38512  cdleme43dN  38513  cdleme46f2g2  38514  cdleme46f2g1  38515  cdleme17d2  38516  cdleme48b  38524  cdleme4gfv  38528  cdlemeg49le  38532  cdlemeg46c  38534  cdlemeg46fvaw  38537  cdlemeg46nlpq  38538  cdlemeg46frv  38546  cdlemeg46rgv  38549  cdlemeg46req  38550  cdlemeg46gfre  38553  cdleme50trn1  38570  cdleme50trn2a  38571  cdleme50trn2  38572  cdleme  38581  cdlemf  38584  trlord  38590  cdlemg2ce  38613  cdlemg7fvbwN  38628  cdlemg7aN  38646  cdlemg10bALTN  38657  cdlemg10a  38661  cdlemg10  38662  cdlemg12d  38667  cdlemg12f  38669  cdlemg12g  38670  cdlemg12  38671  cdlemg13a  38672  cdlemg13  38673  cdlemg17b  38683  cdlemg17dN  38684  cdlemg17dALTN  38685  cdlemg17e  38686  cdlemg17f  38687  cdlemg17g  38688  cdlemg17h  38689  cdlemg17i  38690  cdlemg17pq  38693  cdlemg17bq  38694  cdlemg17iqN  38695  cdlemg17  38698  cdlemg18d  38702  cdlemg18  38703  cdlemg19a  38704  cdlemg19  38705  cdlemg21  38707  cdlemg27a  38713  cdlemg28a  38714  cdlemg31b0N  38715  cdlemg27b  38717  cdlemg33b0  38722  cdlemg28b  38724  cdlemg28  38725  cdlemg33a  38727  cdlemg33  38732  cdlemg34  38733  cdlemg35  38734  cdlemg36  38735  ltrnco  38740  trlcone  38749  cdlemg44  38754  cdlemg47  38757  cdlemg48  38758  tendococl  38793  tendoplcl  38802  cdlemh1  38836  cdlemi  38841  cdlemj1  38842  cdlemj2  38843  tendocan  38845  cdlemk6  38858  cdlemki  38862  cdlemksat  38867  cdlemksv2  38868  cdlemk7  38869  cdlemk11  38870  cdlemk12  38871  cdlemkoatnle  38872  cdlemkole  38874  cdlemk14  38875  cdlemk15  38876  cdlemk16a  38877  cdlemk16  38878  cdlemk17  38879  cdlemk1u  38880  cdlemk5u  38882  cdlemk6u  38883  cdlemkuat  38887  cdlemk18  38889  cdlemk19  38890  cdlemk12u  38893  cdlemk21N  38894  cdlemk20  38895  cdlemkoatnle-2N  38896  cdlemk13-2N  38897  cdlemkole-2N  38898  cdlemk14-2N  38899  cdlemk15-2N  38900  cdlemk16-2N  38901  cdlemk17-2N  38902  cdlemk18-2N  38907  cdlemk19-2N  38908  cdlemk7u-2N  38909  cdlemk11u-2N  38910  cdlemk12u-2N  38911  cdlemk21-2N  38912  cdlemk20-2N  38913  cdlemk22  38914  cdlemk23-3  38923  cdlemk25-3  38925  cdlemk26b-3  38926  cdlemk27-3  38928  cdlemk28-3  38929  cdlemk33N  38930  cdlemk37  38935  cdlemky  38947  cdlemk11ta  38950  cdlemkid3N  38954  cdlemk11tc  38966  cdlemk11t  38967  cdlemk45  38968  cdlemk46  38969  cdlemk47  38970  cdlemk48  38971  cdlemk49  38972  cdlemk50  38973  cdlemk51  38974  cdlemk52  38975  cdlemk55b  38981  cdlemkyyN  38983  cdlemk55u1  38986  cdlemk55u  38987  cdlemk39u1  38988  cdlemk39u  38989  cdlemk56  38992  cdleml3N  38999  cdleml4N  39000  cdlemm10N  39139  dihord1  39239  dihord2a  39240  dihord2b  39241  dihord10  39244  dihord11c  39245  dihord2pre  39246  dihord4  39279  dihord5apre  39283  dihmeetlem1N  39311  dihglbcpreN  39321  dihjatc1  39332  dihjatc3  39334  dihmeetlem13N  39340  dihmeetlem20N  39347  baerlem3lem2  39731  baerlem5alem2  39732  baerlem5blem2  39733  hdmap14lem11  39899  hdmap14lem12  39900  flt4lem5  40494  monotuz  40770  congmul  40796  congsub  40799  rpnnen3lem  40860  ntrclsiso  41684  ntrclskb  41686  ntrclsk3  41687  wessf1ornlem  42729  infleinf  42918  lincdifsn  45776  itsclc0yqe  46118  itsclc0xyqsolr  46126  iscnrm3rlem8  46252  iscnrm3llem2  46255