Theorem simp11 1222

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp111  1321  simp211  1330  simp311  1339  omeulem1  8576  omeu  8579  ackbij1lem16  10236  coprimeprodsq  16893  pythagtriplem14  16913  pythagtrip  16919  mrelatglb  18641  subglsm  19774  lsmpropd  19778  mdetmul  22817  decpmatid  22964  isfil2  24050  filuni  24079  cxple2a  26901  isosctr  27023  nolesgn2o  27872  nolesgn2ores  27873  nogesgn1o  27874  nogesgn1ores  27875  nolt02o  27896  nogt01o  27897  sltstr  28017  cofcut2  28152  brbtwn2  29292  colinearalg  29297  ax5seglem3  29318  clwwlknonex2  30497  measres  34644  bayesth  34861  ofscom  36520  btwndiff  36540  ifscgr  36557  brofs2  36590  brifs2  36591  fscgr  36593  btwnconn1lem1  36600  btwnconn1lem2  36601  btwnconn1lem3  36602  btwnconn1lem4  36603  btwnconn1lem5  36604  btwnconn1lem6  36605  btwnconn1lem7  36606  btwnconn1lem8  36607  btwnconn1lem9  36608  btwnconn1lem10  36609  btwnconn1lem11  36610  btwnconn1lem12  36611  seglecgr12im  36623  seglecgr12  36624  ivthALT  36887  eqlkr  39914  lkrshp  39920  lshpkrlem5  39929  cvrval3  40228  4noncolr3  40268  4noncolr2  40269  4noncolr1  40270  athgt  40271  3dimlem2  40274  3dimlem3a  40275  3dimlem4a  40278  3dimlem4  40279  3dimlem4OLDN  40280  3dim2  40283  1cvratex  40288  hlatexch4  40296  ps-2b  40297  3atlem1  40298  3atlem2  40299  3atlem4  40301  3atlem5  40302  3atlem6  40303  llnnleat  40328  2atm  40342  ps-2c  40343  llnmlplnN  40354  lplnnlelln  40358  2atmat  40376  2llnjN  40382  lvoli2  40396  lvolnlelln  40399  4atlem3b  40413  4atlem9  40418  4atlem10a  40419  4atlem10  40421  4atlem11a  40422  4atlem11b  40423  4atlem12a  40425  4atlem12b  40426  4at  40428  4at2  40429  lplncvrlvol2  40430  2lplnj  40435  dalemswapyz  40471  dath2  40552  lneq2at  40593  2lnat  40599  cdlema1N  40606  cdlemb  40609  paddasslem15  40649  pmodlem1  40661  llnmod2i2  40678  llnexchb2lem  40683  llnexchb2  40684  dalawlem1  40686  dalawlem3  40688  dalawlem4  40689  dalawlem5  40690  dalawlem6  40691  dalawlem7  40692  dalawlem8  40693  dalawlem9  40694  dalawlem10  40695  dalawlem11  40696  dalawlem12  40697  dalawlem13  40698  dalawlem15  40700  dalaw  40701  osumcllem5N  40775  osumcllem6N  40776  osumcllem7N  40777  osumcllem9N  40779  osumcllem10N  40780  osumcllem11N  40781  pl42lem1N  40794  lhpexle3lem  40826  lhpmcvr5N  40842  lhp2atne  40849  lhp2at0ne  40851  4atexlemswapqr  40878  4atexlemex6  40889  ldilco  40931  ltrneq  40964  trlval2  40978  trlnidat  40988  cdlemd2  41014  cdlemd7  41019  cdlemd8  41020  cdleme7aa  41057  cdleme7c  41060  cdleme7d  41061  cdleme7e  41062  cdleme7ga  41063  cdleme7  41064  cdleme11c  41076  cdleme11e  41078  cdleme11l  41084  cdleme11  41085  cdleme14  41088  cdleme15a  41089  cdleme15c  41091  cdleme16b  41094  cdleme16c  41095  cdleme16d  41096  cdleme16e  41097  cdleme16f  41098  cdleme0nex  41105  cdleme18d  41110  cdleme19b  41119  cdleme19d  41121  cdleme19e  41122  cdleme20f  41129  cdleme20i  41132  cdleme20k  41134  cdleme20l1  41135  cdleme20l2  41136  cdleme20l  41137  cdleme20m  41138  cdleme21a  41140  cdleme21b  41141  cdleme21ct  41144  cdleme21d  41145  cdleme21e  41146  cdleme21f  41147  cdleme21h  41149  cdleme22eALTN  41160  cdleme22f2  41162  cdleme22g  41163  cdleme26e  41174  cdleme26eALTN  41176  cdleme26fALTN  41177  cdleme26f  41178  cdleme26f2ALTN  41179  cdleme26f2  41180  cdleme28a  41185  cdleme28b  41186  cdleme28  41188  cdleme29ex  41189  cdleme29c  41191  cdlemefrs29cpre1  41213  cdlemefr29exN  41217  cdlemefr32sn2aw  41219  cdlemefr29bpre0N  41221  cdlemefr29clN  41222  cdlemefr32fvaN  41224  cdlemefr32fva1  41225  cdlemefs32sn1aw  41229  cdleme43fsv1snlem  41235  cdleme41sn3a  41248  cdleme32fva  41252  cdleme32b  41257  cdleme32d  41259  cdleme32e  41260  cdleme32f  41261  cdleme32le  41262  cdleme35a  41263  cdleme35fnpq  41264  cdleme35b  41265  cdleme35c  41266  cdleme35d  41267  cdleme35e  41268  cdleme35f  41269  cdleme36a  41275  cdleme36m  41276  cdleme37m  41277  cdleme39a  41280  cdleme39n  41281  cdleme40m  41282  cdleme40n  41283  cdleme42e  41294  cdleme42f  41295  cdleme42g  41296  cdleme43bN  41305  cdleme43cN  41306  cdleme43dN  41307  cdleme46f2g2  41308  cdleme46f2g1  41309  cdleme17d2  41310  cdleme48b  41318  cdleme4gfv  41322  cdlemeg49le  41326  cdlemeg46c  41328  cdlemeg46fvaw  41331  cdlemeg46nlpq  41332  cdlemeg46frv  41340  cdlemeg46rgv  41343  cdlemeg46req  41344  cdlemeg46gfre  41347  cdleme50trn1  41364  cdleme50trn2a  41365  cdleme50trn2  41366  cdleme  41375  cdlemf  41378  trlord  41384  cdlemg2ce  41407  cdlemg7fvbwN  41422  cdlemg7aN  41440  cdlemg10bALTN  41451  cdlemg10a  41455  cdlemg10  41456  cdlemg12d  41461  cdlemg12f  41463  cdlemg12g  41464  cdlemg12  41465  cdlemg13a  41466  cdlemg13  41467  cdlemg17b  41477  cdlemg17dN  41478  cdlemg17dALTN  41479  cdlemg17e  41480  cdlemg17f  41481  cdlemg17g  41482  cdlemg17h  41483  cdlemg17i  41484  cdlemg17pq  41487  cdlemg17bq  41488  cdlemg17iqN  41489  cdlemg17  41492  cdlemg18d  41496  cdlemg18  41497  cdlemg19a  41498  cdlemg19  41499  cdlemg21  41501  cdlemg27a  41507  cdlemg28a  41508  cdlemg31b0N  41509  cdlemg27b  41511  cdlemg33b0  41516  cdlemg28b  41518  cdlemg28  41519  cdlemg33a  41521  cdlemg33  41526  cdlemg34  41527  cdlemg35  41528  cdlemg36  41529  ltrnco  41534  trlcone  41543  cdlemg44  41548  cdlemg47  41551  cdlemg48  41552  tendococl  41587  tendoplcl  41596  cdlemh1  41630  cdlemi  41635  cdlemj1  41636  cdlemj2  41637  tendocan  41639  cdlemk6  41652  cdlemki  41656  cdlemksat  41661  cdlemksv2  41662  cdlemk7  41663  cdlemk11  41664  cdlemk12  41665  cdlemkoatnle  41666  cdlemkole  41668  cdlemk14  41669  cdlemk15  41670  cdlemk16a  41671  cdlemk16  41672  cdlemk17  41673  cdlemk1u  41674  cdlemk5u  41676  cdlemk6u  41677  cdlemkuat  41681  cdlemk18  41683  cdlemk19  41684  cdlemk12u  41687  cdlemk21N  41688  cdlemk20  41689  cdlemkoatnle-2N  41690  cdlemk13-2N  41691  cdlemkole-2N  41692  cdlemk14-2N  41693  cdlemk15-2N  41694  cdlemk16-2N  41695  cdlemk17-2N  41696  cdlemk18-2N  41701  cdlemk19-2N  41702  cdlemk7u-2N  41703  cdlemk11u-2N  41704  cdlemk12u-2N  41705  cdlemk21-2N  41706  cdlemk20-2N  41707  cdlemk22  41708  cdlemk23-3  41717  cdlemk25-3  41719  cdlemk26b-3  41720  cdlemk27-3  41722  cdlemk28-3  41723  cdlemk33N  41724  cdlemk37  41729  cdlemky  41741  cdlemk11ta  41744  cdlemkid3N  41748  cdlemk11tc  41760  cdlemk11t  41761  cdlemk45  41762  cdlemk46  41763  cdlemk47  41764  cdlemk48  41765  cdlemk49  41766  cdlemk50  41767  cdlemk51  41768  cdlemk52  41769  cdlemk55b  41775  cdlemkyyN  41777  cdlemk55u1  41780  cdlemk55u  41781  cdlemk39u1  41782  cdlemk39u  41783  cdlemk56  41786  cdleml3N  41793  cdleml4N  41794  cdlemm10N  41933  dihord1  42033  dihord2a  42034  dihord2b  42035  dihord10  42038  dihord11c  42039  dihord2pre  42040  dihord4  42073  dihord5apre  42077  dihmeetlem1N  42105  dihglbcpreN  42115  dihjatc1  42126  dihjatc3  42128  dihmeetlem13N  42134  dihmeetlem20N  42141  baerlem3lem2  42525  baerlem5alem2  42526  baerlem5blem2  42527  hdmap14lem11  42693  hdmap14lem12  42694  flt4lem5  43423  monotuz  43709  congmul  43735  congsub  43738  rpnnen3lem  43799  ntrclsiso  44834  ntrclskb  44836  ntrclsk3  44837  wessf1ornlem  45944  infleinf  46128  lincdifsn  49245  itsclc0yqe  49582  itsclc0xyqsolr  49590  iscnrm3rlem8  49766  iscnrm3llem2  49769