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  8590  omeu  8593  ackbij1lem16  10312  coprimeprodsq  16986  pythagtriplem14  17006  pythagtrip  17012  mrelatglb  18734  subglsm  19887  lsmpropd  19891  mdetmul  22938  decpmatid  23088  isfil2  24175  filuni  24204  cxple2a  27027  isosctr  27149  flt4lem5  27980  nolesgn2o  28028  nolesgn2ores  28029  nogesgn1o  28030  nogesgn1ores  28031  nolt02o  28052  nogt01o  28053  sltstr  28173  cofcut2  28308  brbtwn2  29483  colinearalg  29488  ax5seglem3  29509  clwwlknonex2  30700  measres  34897  bayesth  35113  ofscom  36814  btwndiff  36834  ifscgr  36851  brofs2  36884  brifs2  36885  fscgr  36887  btwnconn1lem1  36894  btwnconn1lem2  36895  btwnconn1lem3  36896  btwnconn1lem4  36897  btwnconn1lem5  36898  btwnconn1lem6  36899  btwnconn1lem7  36900  btwnconn1lem8  36901  btwnconn1lem9  36902  btwnconn1lem10  36903  btwnconn1lem11  36904  btwnconn1lem12  36905  seglecgr12im  36917  seglecgr12  36918  ivthALT  37165  eqlkr  40199  lkrshp  40205  lshpkrlem5  40214  cvrval3  40513  4noncolr3  40553  4noncolr2  40554  4noncolr1  40555  athgt  40556  3dimlem2  40559  3dimlem3a  40560  3dimlem4a  40563  3dimlem4  40564  3dimlem4OLDN  40565  3dim2  40568  1cvratex  40573  hlatexch4  40581  ps-2b  40582  3atlem1  40583  3atlem2  40584  3atlem4  40586  3atlem5  40587  3atlem6  40588  llnnleat  40613  2atm  40627  ps-2c  40628  llnmlplnN  40639  lplnnlelln  40643  2atmat  40661  2llnjN  40667  lvoli2  40681  lvolnlelln  40684  4atlem3b  40698  4atlem9  40703  4atlem10a  40704  4atlem10  40706  4atlem11a  40707  4atlem11b  40708  4atlem12a  40710  4atlem12b  40711  4at  40713  4at2  40714  lplncvrlvol2  40715  2lplnj  40720  dalemswapyz  40756  dath2  40837  lneq2at  40878  2lnat  40884  cdlema1N  40891  cdlemb  40894  paddasslem15  40934  pmodlem1  40946  llnmod2i2  40963  llnexchb2lem  40968  llnexchb2  40969  dalawlem1  40971  dalawlem3  40973  dalawlem4  40974  dalawlem5  40975  dalawlem6  40976  dalawlem7  40977  dalawlem8  40978  dalawlem9  40979  dalawlem10  40980  dalawlem11  40981  dalawlem12  40982  dalawlem13  40983  dalawlem15  40985  dalaw  40986  osumcllem5N  41060  osumcllem6N  41061  osumcllem7N  41062  osumcllem9N  41064  osumcllem10N  41065  osumcllem11N  41066  pl42lem1N  41079  lhpexle3lem  41111  lhpmcvr5N  41127  lhp2atne  41134  lhp2at0ne  41136  4atexlemswapqr  41163  4atexlemex6  41174  ldilco  41216  ltrneq  41249  trlval2  41263  trlnidat  41273  cdlemd2  41299  cdlemd7  41304  cdlemd8  41305  cdleme7aa  41342  cdleme7c  41345  cdleme7d  41346  cdleme7e  41347  cdleme7ga  41348  cdleme7  41349  cdleme11c  41361  cdleme11e  41363  cdleme11l  41369  cdleme11  41370  cdleme14  41373  cdleme15a  41374  cdleme15c  41376  cdleme16b  41379  cdleme16c  41380  cdleme16d  41381  cdleme16e  41382  cdleme16f  41383  cdleme0nex  41390  cdleme18d  41395  cdleme19b  41404  cdleme19d  41406  cdleme19e  41407  cdleme20f  41414  cdleme20i  41417  cdleme20k  41419  cdleme20l1  41420  cdleme20l2  41421  cdleme20l  41422  cdleme20m  41423  cdleme21a  41425  cdleme21b  41426  cdleme21ct  41429  cdleme21d  41430  cdleme21e  41431  cdleme21f  41432  cdleme21h  41434  cdleme22eALTN  41445  cdleme22f2  41447  cdleme22g  41448  cdleme26e  41459  cdleme26eALTN  41461  cdleme26fALTN  41462  cdleme26f  41463  cdleme26f2ALTN  41464  cdleme26f2  41465  cdleme28a  41470  cdleme28b  41471  cdleme28  41473  cdleme29ex  41474  cdleme29c  41476  cdlemefrs29cpre1  41498  cdlemefr29exN  41502  cdlemefr32sn2aw  41504  cdlemefr29bpre0N  41506  cdlemefr29clN  41507  cdlemefr32fvaN  41509  cdlemefr32fva1  41510  cdlemefs32sn1aw  41514  cdleme43fsv1snlem  41520  cdleme41sn3a  41533  cdleme32fva  41537  cdleme32b  41542  cdleme32d  41544  cdleme32e  41545  cdleme32f  41546  cdleme32le  41547  cdleme35a  41548  cdleme35fnpq  41549  cdleme35b  41550  cdleme35c  41551  cdleme35d  41552  cdleme35e  41553  cdleme35f  41554  cdleme36a  41560  cdleme36m  41561  cdleme37m  41562  cdleme39a  41565  cdleme39n  41566  cdleme40m  41567  cdleme40n  41568  cdleme42e  41579  cdleme42f  41580  cdleme42g  41581  cdleme43bN  41590  cdleme43cN  41591  cdleme43dN  41592  cdleme46f2g2  41593  cdleme46f2g1  41594  cdleme17d2  41595  cdleme48b  41603  cdleme4gfv  41607  cdlemeg49le  41611  cdlemeg46c  41613  cdlemeg46fvaw  41616  cdlemeg46nlpq  41617  cdlemeg46frv  41625  cdlemeg46rgv  41628  cdlemeg46req  41629  cdlemeg46gfre  41632  cdleme50trn1  41649  cdleme50trn2a  41650  cdleme50trn2  41651  cdleme  41660  cdlemf  41663  trlord  41669  cdlemg2ce  41692  cdlemg7fvbwN  41707  cdlemg7aN  41725  cdlemg10bALTN  41736  cdlemg10a  41740  cdlemg10  41741  cdlemg12d  41746  cdlemg12f  41748  cdlemg12g  41749  cdlemg12  41750  cdlemg13a  41751  cdlemg13  41752  cdlemg17b  41762  cdlemg17dN  41763  cdlemg17dALTN  41764  cdlemg17e  41765  cdlemg17f  41766  cdlemg17g  41767  cdlemg17h  41768  cdlemg17i  41769  cdlemg17pq  41772  cdlemg17bq  41773  cdlemg17iqN  41774  cdlemg17  41777  cdlemg18d  41781  cdlemg18  41782  cdlemg19a  41783  cdlemg19  41784  cdlemg21  41786  cdlemg27a  41792  cdlemg28a  41793  cdlemg31b0N  41794  cdlemg27b  41796  cdlemg33b0  41801  cdlemg28b  41803  cdlemg28  41804  cdlemg33a  41806  cdlemg33  41811  cdlemg34  41812  cdlemg35  41813  cdlemg36  41814  ltrnco  41819  trlcone  41828  cdlemg44  41833  cdlemg47  41836  cdlemg48  41837  tendococl  41872  tendoplcl  41881  cdlemh1  41915  cdlemi  41920  cdlemj1  41921  cdlemj2  41922  tendocan  41924  cdlemk6  41937  cdlemki  41941  cdlemksat  41946  cdlemksv2  41947  cdlemk7  41948  cdlemk11  41949  cdlemk12  41950  cdlemkoatnle  41951  cdlemkole  41953  cdlemk14  41954  cdlemk15  41955  cdlemk16a  41956  cdlemk16  41957  cdlemk17  41958  cdlemk1u  41959  cdlemk5u  41961  cdlemk6u  41962  cdlemkuat  41966  cdlemk18  41968  cdlemk19  41969  cdlemk12u  41972  cdlemk21N  41973  cdlemk20  41974  cdlemkoatnle-2N  41975  cdlemk13-2N  41976  cdlemkole-2N  41977  cdlemk14-2N  41978  cdlemk15-2N  41979  cdlemk16-2N  41980  cdlemk17-2N  41981  cdlemk18-2N  41986  cdlemk19-2N  41987  cdlemk7u-2N  41988  cdlemk11u-2N  41989  cdlemk12u-2N  41990  cdlemk21-2N  41991  cdlemk20-2N  41992  cdlemk22  41993  cdlemk23-3  42002  cdlemk25-3  42004  cdlemk26b-3  42005  cdlemk27-3  42007  cdlemk28-3  42008  cdlemk33N  42009  cdlemk37  42014  cdlemky  42026  cdlemk11ta  42029  cdlemkid3N  42033  cdlemk11tc  42045  cdlemk11t  42046  cdlemk45  42047  cdlemk46  42048  cdlemk47  42049  cdlemk48  42050  cdlemk49  42051  cdlemk50  42052  cdlemk51  42053  cdlemk52  42054  cdlemk55b  42060  cdlemkyyN  42062  cdlemk55u1  42065  cdlemk55u  42066  cdlemk39u1  42067  cdlemk39u  42068  cdlemk56  42071  cdleml3N  42078  cdleml4N  42079  cdlemm10N  42218  dihord1  42318  dihord2a  42319  dihord2b  42320  dihord10  42323  dihord11c  42324  dihord2pre  42325  dihord4  42358  dihord5apre  42362  dihmeetlem1N  42390  dihglbcpreN  42400  dihjatc1  42411  dihjatc3  42413  dihmeetlem13N  42419  dihmeetlem20N  42426  baerlem3lem2  42810  baerlem5alem2  42811  baerlem5blem2  42812  hdmap14lem11  42978  hdmap14lem12  42979  monotuz  43990  congmul  44016  congsub  44019  rpnnen3lem  44080  ntrclsiso  45109  ntrclskb  45111  ntrclsk3  45112  dmstructnn  45968  wessf1ornlem  46242  infleinf  46425  lincdifsn  49578  itsclc0yqe  49915  itsclc0xyqsolr  49923  iscnrm3rlem8  50097  iscnrm3llem2  50100