Theorem simp11 1204

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 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp111  1303  simp211  1312  simp311  1321  omeulem1  8497  omeu  8500  ackbij1lem16  10125  coprimeprodsq  16720  pythagtriplem14  16740  pythagtrip  16746  mrelatglb  18466  subglsm  19586  lsmpropd  19590  mdetmul  22539  decpmatid  22686  isfil2  23772  filuni  23801  cxple2a  26636  isosctr  26759  nolesgn2o  27611  nolesgn2ores  27612  nogesgn1o  27613  nogesgn1ores  27614  nolt02o  27635  nogt01o  27636  sslttr  27749  cofcut2  27867  brbtwn2  28884  colinearalg  28889  ax5seglem3  28910  clwwlknonex2  30087  measres  34233  bayesth  34450  ofscom  36047  btwndiff  36067  ifscgr  36084  brofs2  36117  brifs2  36118  fscgr  36120  btwnconn1lem1  36127  btwnconn1lem2  36128  btwnconn1lem3  36129  btwnconn1lem4  36130  btwnconn1lem5  36131  btwnconn1lem6  36132  btwnconn1lem7  36133  btwnconn1lem8  36134  btwnconn1lem9  36135  btwnconn1lem10  36136  btwnconn1lem11  36137  btwnconn1lem12  36138  seglecgr12im  36150  seglecgr12  36151  ivthALT  36375  eqlkr  39144  lkrshp  39150  lshpkrlem5  39159  cvrval3  39458  4noncolr3  39498  4noncolr2  39499  4noncolr1  39500  athgt  39501  3dimlem2  39504  3dimlem3a  39505  3dimlem4a  39508  3dimlem4  39509  3dimlem4OLDN  39510  3dim2  39513  1cvratex  39518  hlatexch4  39526  ps-2b  39527  3atlem1  39528  3atlem2  39529  3atlem4  39531  3atlem5  39532  3atlem6  39533  llnnleat  39558  2atm  39572  ps-2c  39573  llnmlplnN  39584  lplnnlelln  39588  2atmat  39606  2llnjN  39612  lvoli2  39626  lvolnlelln  39629  4atlem3b  39643  4atlem9  39648  4atlem10a  39649  4atlem10  39651  4atlem11a  39652  4atlem11b  39653  4atlem12a  39655  4atlem12b  39656  4at  39658  4at2  39659  lplncvrlvol2  39660  2lplnj  39665  dalemswapyz  39701  dath2  39782  lneq2at  39823  2lnat  39829  cdlema1N  39836  cdlemb  39839  paddasslem15  39879  pmodlem1  39891  llnmod2i2  39908  llnexchb2lem  39913  llnexchb2  39914  dalawlem1  39916  dalawlem3  39918  dalawlem4  39919  dalawlem5  39920  dalawlem6  39921  dalawlem7  39922  dalawlem8  39923  dalawlem9  39924  dalawlem10  39925  dalawlem11  39926  dalawlem12  39927  dalawlem13  39928  dalawlem15  39930  dalaw  39931  osumcllem5N  40005  osumcllem6N  40006  osumcllem7N  40007  osumcllem9N  40009  osumcllem10N  40010  osumcllem11N  40011  pl42lem1N  40024  lhpexle3lem  40056  lhpmcvr5N  40072  lhp2atne  40079  lhp2at0ne  40081  4atexlemswapqr  40108  4atexlemex6  40119  ldilco  40161  ltrneq  40194  trlval2  40208  trlnidat  40218  cdlemd2  40244  cdlemd7  40249  cdlemd8  40250  cdleme7aa  40287  cdleme7c  40290  cdleme7d  40291  cdleme7e  40292  cdleme7ga  40293  cdleme7  40294  cdleme11c  40306  cdleme11e  40308  cdleme11l  40314  cdleme11  40315  cdleme14  40318  cdleme15a  40319  cdleme15c  40321  cdleme16b  40324  cdleme16c  40325  cdleme16d  40326  cdleme16e  40327  cdleme16f  40328  cdleme0nex  40335  cdleme18d  40340  cdleme19b  40349  cdleme19d  40351  cdleme19e  40352  cdleme20f  40359  cdleme20i  40362  cdleme20k  40364  cdleme20l1  40365  cdleme20l2  40366  cdleme20l  40367  cdleme20m  40368  cdleme21a  40370  cdleme21b  40371  cdleme21ct  40374  cdleme21d  40375  cdleme21e  40376  cdleme21f  40377  cdleme21h  40379  cdleme22eALTN  40390  cdleme22f2  40392  cdleme22g  40393  cdleme26e  40404  cdleme26eALTN  40406  cdleme26fALTN  40407  cdleme26f  40408  cdleme26f2ALTN  40409  cdleme26f2  40410  cdleme28a  40415  cdleme28b  40416  cdleme28  40418  cdleme29ex  40419  cdleme29c  40421  cdlemefrs29cpre1  40443  cdlemefr29exN  40447  cdlemefr32sn2aw  40449  cdlemefr29bpre0N  40451  cdlemefr29clN  40452  cdlemefr32fvaN  40454  cdlemefr32fva1  40455  cdlemefs32sn1aw  40459  cdleme43fsv1snlem  40465  cdleme41sn3a  40478  cdleme32fva  40482  cdleme32b  40487  cdleme32d  40489  cdleme32e  40490  cdleme32f  40491  cdleme32le  40492  cdleme35a  40493  cdleme35fnpq  40494  cdleme35b  40495  cdleme35c  40496  cdleme35d  40497  cdleme35e  40498  cdleme35f  40499  cdleme36a  40505  cdleme36m  40506  cdleme37m  40507  cdleme39a  40510  cdleme39n  40511  cdleme40m  40512  cdleme40n  40513  cdleme42e  40524  cdleme42f  40525  cdleme42g  40526  cdleme43bN  40535  cdleme43cN  40536  cdleme43dN  40537  cdleme46f2g2  40538  cdleme46f2g1  40539  cdleme17d2  40540  cdleme48b  40548  cdleme4gfv  40552  cdlemeg49le  40556  cdlemeg46c  40558  cdlemeg46fvaw  40561  cdlemeg46nlpq  40562  cdlemeg46frv  40570  cdlemeg46rgv  40573  cdlemeg46req  40574  cdlemeg46gfre  40577  cdleme50trn1  40594  cdleme50trn2a  40595  cdleme50trn2  40596  cdleme  40605  cdlemf  40608  trlord  40614  cdlemg2ce  40637  cdlemg7fvbwN  40652  cdlemg7aN  40670  cdlemg10bALTN  40681  cdlemg10a  40685  cdlemg10  40686  cdlemg12d  40691  cdlemg12f  40693  cdlemg12g  40694  cdlemg12  40695  cdlemg13a  40696  cdlemg13  40697  cdlemg17b  40707  cdlemg17dN  40708  cdlemg17dALTN  40709  cdlemg17e  40710  cdlemg17f  40711  cdlemg17g  40712  cdlemg17h  40713  cdlemg17i  40714  cdlemg17pq  40717  cdlemg17bq  40718  cdlemg17iqN  40719  cdlemg17  40722  cdlemg18d  40726  cdlemg18  40727  cdlemg19a  40728  cdlemg19  40729  cdlemg21  40731  cdlemg27a  40737  cdlemg28a  40738  cdlemg31b0N  40739  cdlemg27b  40741  cdlemg33b0  40746  cdlemg28b  40748  cdlemg28  40749  cdlemg33a  40751  cdlemg33  40756  cdlemg34  40757  cdlemg35  40758  cdlemg36  40759  ltrnco  40764  trlcone  40773  cdlemg44  40778  cdlemg47  40781  cdlemg48  40782  tendococl  40817  tendoplcl  40826  cdlemh1  40860  cdlemi  40865  cdlemj1  40866  cdlemj2  40867  tendocan  40869  cdlemk6  40882  cdlemki  40886  cdlemksat  40891  cdlemksv2  40892  cdlemk7  40893  cdlemk11  40894  cdlemk12  40895  cdlemkoatnle  40896  cdlemkole  40898  cdlemk14  40899  cdlemk15  40900  cdlemk16a  40901  cdlemk16  40902  cdlemk17  40903  cdlemk1u  40904  cdlemk5u  40906  cdlemk6u  40907  cdlemkuat  40911  cdlemk18  40913  cdlemk19  40914  cdlemk12u  40917  cdlemk21N  40918  cdlemk20  40919  cdlemkoatnle-2N  40920  cdlemk13-2N  40921  cdlemkole-2N  40922  cdlemk14-2N  40923  cdlemk15-2N  40924  cdlemk16-2N  40925  cdlemk17-2N  40926  cdlemk18-2N  40931  cdlemk19-2N  40932  cdlemk7u-2N  40933  cdlemk11u-2N  40934  cdlemk12u-2N  40935  cdlemk21-2N  40936  cdlemk20-2N  40937  cdlemk22  40938  cdlemk23-3  40947  cdlemk25-3  40949  cdlemk26b-3  40950  cdlemk27-3  40952  cdlemk28-3  40953  cdlemk33N  40954  cdlemk37  40959  cdlemky  40971  cdlemk11ta  40974  cdlemkid3N  40978  cdlemk11tc  40990  cdlemk11t  40991  cdlemk45  40992  cdlemk46  40993  cdlemk47  40994  cdlemk48  40995  cdlemk49  40996  cdlemk50  40997  cdlemk51  40998  cdlemk52  40999  cdlemk55b  41005  cdlemkyyN  41007  cdlemk55u1  41010  cdlemk55u  41011  cdlemk39u1  41012  cdlemk39u  41013  cdlemk56  41016  cdleml3N  41023  cdleml4N  41024  cdlemm10N  41163  dihord1  41263  dihord2a  41264  dihord2b  41265  dihord10  41268  dihord11c  41269  dihord2pre  41270  dihord4  41303  dihord5apre  41307  dihmeetlem1N  41335  dihglbcpreN  41345  dihjatc1  41356  dihjatc3  41358  dihmeetlem13N  41364  dihmeetlem20N  41371  baerlem3lem2  41755  baerlem5alem2  41756  baerlem5blem2  41757  hdmap14lem11  41923  hdmap14lem12  41924  flt4lem5  42689  monotuz  42980  congmul  43006  congsub  43009  rpnnen3lem  43070  ntrclsiso  44106  ntrclskb  44108  ntrclsk3  44109  wessf1ornlem  45228  infleinf  45416  lincdifsn  48462  itsclc0yqe  48799  itsclc0xyqsolr  48807  iscnrm3rlem8  48984  iscnrm3llem2  48987