Theorem simp11 1210

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp111  1309  simp211  1318  simp311  1327  omeulem1  8514  omeu  8517  ackbij1lem16  10154  coprimeprodsq  16777  pythagtriplem14  16797  pythagtrip  16803  mrelatglb  18524  subglsm  19646  lsmpropd  19650  mdetmul  22613  decpmatid  22760  isfil2  23846  filuni  23875  cxple2a  26688  isosctr  26810  nolesgn2o  27660  nolesgn2ores  27661  nogesgn1o  27662  nogesgn1ores  27663  nolt02o  27684  nogt01o  27685  sltstr  27804  cofcut2  27939  brbtwn2  28999  colinearalg  29004  ax5seglem3  29025  clwwlknonex2  30204  measres  34413  bayesth  34630  ofscom  36242  btwndiff  36262  ifscgr  36279  brofs2  36312  brifs2  36313  fscgr  36315  btwnconn1lem1  36322  btwnconn1lem2  36323  btwnconn1lem3  36324  btwnconn1lem4  36325  btwnconn1lem5  36326  btwnconn1lem6  36327  btwnconn1lem7  36328  btwnconn1lem8  36329  btwnconn1lem9  36330  btwnconn1lem10  36331  btwnconn1lem11  36332  btwnconn1lem12  36333  seglecgr12im  36345  seglecgr12  36346  ivthALT  36570  eqlkr  39598  lkrshp  39604  lshpkrlem5  39613  cvrval3  39912  4noncolr3  39952  4noncolr2  39953  4noncolr1  39954  athgt  39955  3dimlem2  39958  3dimlem3a  39959  3dimlem4a  39962  3dimlem4  39963  3dimlem4OLDN  39964  3dim2  39967  1cvratex  39972  hlatexch4  39980  ps-2b  39981  3atlem1  39982  3atlem2  39983  3atlem4  39985  3atlem5  39986  3atlem6  39987  llnnleat  40012  2atm  40026  ps-2c  40027  llnmlplnN  40038  lplnnlelln  40042  2atmat  40060  2llnjN  40066  lvoli2  40080  lvolnlelln  40083  4atlem3b  40097  4atlem9  40102  4atlem10a  40103  4atlem10  40105  4atlem11a  40106  4atlem11b  40107  4atlem12a  40109  4atlem12b  40110  4at  40112  4at2  40113  lplncvrlvol2  40114  2lplnj  40119  dalemswapyz  40155  dath2  40236  lneq2at  40277  2lnat  40283  cdlema1N  40290  cdlemb  40293  paddasslem15  40333  pmodlem1  40345  llnmod2i2  40362  llnexchb2lem  40367  llnexchb2  40368  dalawlem1  40370  dalawlem3  40372  dalawlem4  40373  dalawlem5  40374  dalawlem6  40375  dalawlem7  40376  dalawlem8  40377  dalawlem9  40378  dalawlem10  40379  dalawlem11  40380  dalawlem12  40381  dalawlem13  40382  dalawlem15  40384  dalaw  40385  osumcllem5N  40459  osumcllem6N  40460  osumcllem7N  40461  osumcllem9N  40463  osumcllem10N  40464  osumcllem11N  40465  pl42lem1N  40478  lhpexle3lem  40510  lhpmcvr5N  40526  lhp2atne  40533  lhp2at0ne  40535  4atexlemswapqr  40562  4atexlemex6  40573  ldilco  40615  ltrneq  40648  trlval2  40662  trlnidat  40672  cdlemd2  40698  cdlemd7  40703  cdlemd8  40704  cdleme7aa  40741  cdleme7c  40744  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme7  40748  cdleme11c  40760  cdleme11e  40762  cdleme11l  40768  cdleme11  40769  cdleme14  40772  cdleme15a  40773  cdleme15c  40775  cdleme16b  40778  cdleme16c  40779  cdleme16d  40780  cdleme16e  40781  cdleme16f  40782  cdleme0nex  40789  cdleme18d  40794  cdleme19b  40803  cdleme19d  40805  cdleme19e  40806  cdleme20f  40813  cdleme20i  40816  cdleme20k  40818  cdleme20l1  40819  cdleme20l2  40820  cdleme20l  40821  cdleme20m  40822  cdleme21a  40824  cdleme21b  40825  cdleme21ct  40828  cdleme21d  40829  cdleme21e  40830  cdleme21f  40831  cdleme21h  40833  cdleme22eALTN  40844  cdleme22f2  40846  cdleme22g  40847  cdleme26e  40858  cdleme26eALTN  40860  cdleme26fALTN  40861  cdleme26f  40862  cdleme26f2ALTN  40863  cdleme26f2  40864  cdleme28a  40869  cdleme28b  40870  cdleme28  40872  cdleme29ex  40873  cdleme29c  40875  cdlemefrs29cpre1  40897  cdlemefr29exN  40901  cdlemefr32sn2aw  40903  cdlemefr29bpre0N  40905  cdlemefr29clN  40906  cdlemefr32fvaN  40908  cdlemefr32fva1  40909  cdlemefs32sn1aw  40913  cdleme43fsv1snlem  40919  cdleme41sn3a  40932  cdleme32fva  40936  cdleme32b  40941  cdleme32d  40943  cdleme32e  40944  cdleme32f  40945  cdleme32le  40946  cdleme35a  40947  cdleme35fnpq  40948  cdleme35b  40949  cdleme35c  40950  cdleme35d  40951  cdleme35e  40952  cdleme35f  40953  cdleme36a  40959  cdleme36m  40960  cdleme37m  40961  cdleme39a  40964  cdleme39n  40965  cdleme40m  40966  cdleme40n  40967  cdleme42e  40978  cdleme42f  40979  cdleme42g  40980  cdleme43bN  40989  cdleme43cN  40990  cdleme43dN  40991  cdleme46f2g2  40992  cdleme46f2g1  40993  cdleme17d2  40994  cdleme48b  41002  cdleme4gfv  41006  cdlemeg49le  41010  cdlemeg46c  41012  cdlemeg46fvaw  41015  cdlemeg46nlpq  41016  cdlemeg46frv  41024  cdlemeg46rgv  41027  cdlemeg46req  41028  cdlemeg46gfre  41031  cdleme50trn1  41048  cdleme50trn2a  41049  cdleme50trn2  41050  cdleme  41059  cdlemf  41062  trlord  41068  cdlemg2ce  41091  cdlemg7fvbwN  41106  cdlemg7aN  41124  cdlemg10bALTN  41135  cdlemg10a  41139  cdlemg10  41140  cdlemg12d  41145  cdlemg12f  41147  cdlemg12g  41148  cdlemg12  41149  cdlemg13a  41150  cdlemg13  41151  cdlemg17b  41161  cdlemg17dN  41162  cdlemg17dALTN  41163  cdlemg17e  41164  cdlemg17f  41165  cdlemg17g  41166  cdlemg17h  41167  cdlemg17i  41168  cdlemg17pq  41171  cdlemg17bq  41172  cdlemg17iqN  41173  cdlemg17  41176  cdlemg18d  41180  cdlemg18  41181  cdlemg19a  41182  cdlemg19  41183  cdlemg21  41185  cdlemg27a  41191  cdlemg28a  41192  cdlemg31b0N  41193  cdlemg27b  41195  cdlemg33b0  41200  cdlemg28b  41202  cdlemg28  41203  cdlemg33a  41205  cdlemg33  41210  cdlemg34  41211  cdlemg35  41212  cdlemg36  41213  ltrnco  41218  trlcone  41227  cdlemg44  41232  cdlemg47  41235  cdlemg48  41236  tendococl  41271  tendoplcl  41280  cdlemh1  41314  cdlemi  41319  cdlemj1  41320  cdlemj2  41321  tendocan  41323  cdlemk6  41336  cdlemki  41340  cdlemksat  41345  cdlemksv2  41346  cdlemk7  41347  cdlemk11  41348  cdlemk12  41349  cdlemkoatnle  41350  cdlemkole  41352  cdlemk14  41353  cdlemk15  41354  cdlemk16a  41355  cdlemk16  41356  cdlemk17  41357  cdlemk1u  41358  cdlemk5u  41360  cdlemk6u  41361  cdlemkuat  41365  cdlemk18  41367  cdlemk19  41368  cdlemk12u  41371  cdlemk21N  41372  cdlemk20  41373  cdlemkoatnle-2N  41374  cdlemk13-2N  41375  cdlemkole-2N  41376  cdlemk14-2N  41377  cdlemk15-2N  41378  cdlemk16-2N  41379  cdlemk17-2N  41380  cdlemk18-2N  41385  cdlemk19-2N  41386  cdlemk7u-2N  41387  cdlemk11u-2N  41388  cdlemk12u-2N  41389  cdlemk21-2N  41390  cdlemk20-2N  41391  cdlemk22  41392  cdlemk23-3  41401  cdlemk25-3  41403  cdlemk26b-3  41404  cdlemk27-3  41406  cdlemk28-3  41407  cdlemk33N  41408  cdlemk37  41413  cdlemky  41425  cdlemk11ta  41428  cdlemkid3N  41432  cdlemk11tc  41444  cdlemk11t  41445  cdlemk45  41446  cdlemk46  41447  cdlemk47  41448  cdlemk48  41449  cdlemk49  41450  cdlemk50  41451  cdlemk51  41452  cdlemk52  41453  cdlemk55b  41459  cdlemkyyN  41461  cdlemk55u1  41464  cdlemk55u  41465  cdlemk39u1  41466  cdlemk39u  41467  cdlemk56  41470  cdleml3N  41477  cdleml4N  41478  cdlemm10N  41617  dihord1  41717  dihord2a  41718  dihord2b  41719  dihord10  41722  dihord11c  41723  dihord2pre  41724  dihord4  41757  dihord5apre  41761  dihmeetlem1N  41789  dihglbcpreN  41799  dihjatc1  41810  dihjatc3  41812  dihmeetlem13N  41818  dihmeetlem20N  41825  baerlem3lem2  42209  baerlem5alem2  42210  baerlem5blem2  42211  hdmap14lem11  42377  hdmap14lem12  42378  flt4lem5  43107  monotuz  43393  congmul  43419  congsub  43422  rpnnen3lem  43483  ntrclsiso  44518  ntrclskb  44520  ntrclsk3  44521  wessf1ornlem  45639  infleinf  45823  lincdifsn  48922  itsclc0yqe  49259  itsclc0xyqsolr  49267  iscnrm3rlem8  49444  iscnrm3llem2  49447