Theorem simp11 1205

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp111  1304  simp211  1313  simp311  1322  omeulem1  8517  omeu  8520  ackbij1lem16  10156  coprimeprodsq  16779  pythagtriplem14  16799  pythagtrip  16805  mrelatglb  18526  subglsm  19648  lsmpropd  19652  mdetmul  22588  decpmatid  22735  isfil2  23821  filuni  23850  cxple2a  26663  isosctr  26785  nolesgn2o  27635  nolesgn2ores  27636  nogesgn1o  27637  nogesgn1ores  27638  nolt02o  27659  nogt01o  27660  sltstr  27779  cofcut2  27914  brbtwn2  28974  colinearalg  28979  ax5seglem3  29000  clwwlknonex2  30179  measres  34366  bayesth  34583  ofscom  36189  btwndiff  36209  ifscgr  36226  brofs2  36259  brifs2  36260  fscgr  36262  btwnconn1lem1  36269  btwnconn1lem2  36270  btwnconn1lem3  36271  btwnconn1lem4  36272  btwnconn1lem5  36273  btwnconn1lem6  36274  btwnconn1lem7  36275  btwnconn1lem8  36276  btwnconn1lem9  36277  btwnconn1lem10  36278  btwnconn1lem11  36279  btwnconn1lem12  36280  seglecgr12im  36292  seglecgr12  36293  ivthALT  36517  eqlkr  39545  lkrshp  39551  lshpkrlem5  39560  cvrval3  39859  4noncolr3  39899  4noncolr2  39900  4noncolr1  39901  athgt  39902  3dimlem2  39905  3dimlem3a  39906  3dimlem4a  39909  3dimlem4  39910  3dimlem4OLDN  39911  3dim2  39914  1cvratex  39919  hlatexch4  39927  ps-2b  39928  3atlem1  39929  3atlem2  39930  3atlem4  39932  3atlem5  39933  3atlem6  39934  llnnleat  39959  2atm  39973  ps-2c  39974  llnmlplnN  39985  lplnnlelln  39989  2atmat  40007  2llnjN  40013  lvoli2  40027  lvolnlelln  40030  4atlem3b  40044  4atlem9  40049  4atlem10a  40050  4atlem10  40052  4atlem11a  40053  4atlem11b  40054  4atlem12a  40056  4atlem12b  40057  4at  40059  4at2  40060  lplncvrlvol2  40061  2lplnj  40066  dalemswapyz  40102  dath2  40183  lneq2at  40224  2lnat  40230  cdlema1N  40237  cdlemb  40240  paddasslem15  40280  pmodlem1  40292  llnmod2i2  40309  llnexchb2lem  40314  llnexchb2  40315  dalawlem1  40317  dalawlem3  40319  dalawlem4  40320  dalawlem5  40321  dalawlem6  40322  dalawlem7  40323  dalawlem8  40324  dalawlem9  40325  dalawlem10  40326  dalawlem11  40327  dalawlem12  40328  dalawlem13  40329  dalawlem15  40331  dalaw  40332  osumcllem5N  40406  osumcllem6N  40407  osumcllem7N  40408  osumcllem9N  40410  osumcllem10N  40411  osumcllem11N  40412  pl42lem1N  40425  lhpexle3lem  40457  lhpmcvr5N  40473  lhp2atne  40480  lhp2at0ne  40482  4atexlemswapqr  40509  4atexlemex6  40520  ldilco  40562  ltrneq  40595  trlval2  40609  trlnidat  40619  cdlemd2  40645  cdlemd7  40650  cdlemd8  40651  cdleme7aa  40688  cdleme7c  40691  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme11c  40707  cdleme11e  40709  cdleme11l  40715  cdleme11  40716  cdleme14  40719  cdleme15a  40720  cdleme15c  40722  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme16e  40728  cdleme16f  40729  cdleme0nex  40736  cdleme18d  40741  cdleme19b  40750  cdleme19d  40752  cdleme19e  40753  cdleme20f  40760  cdleme20i  40763  cdleme20k  40765  cdleme20l1  40766  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme21a  40771  cdleme21b  40772  cdleme21ct  40775  cdleme21d  40776  cdleme21e  40777  cdleme21f  40778  cdleme21h  40780  cdleme22eALTN  40791  cdleme22f2  40793  cdleme22g  40794  cdleme26e  40805  cdleme26eALTN  40807  cdleme26fALTN  40808  cdleme26f  40809  cdleme26f2ALTN  40810  cdleme26f2  40811  cdleme28a  40816  cdleme28b  40817  cdleme28  40819  cdleme29ex  40820  cdleme29c  40822  cdlemefrs29cpre1  40844  cdlemefr29exN  40848  cdlemefr32sn2aw  40850  cdlemefr29bpre0N  40852  cdlemefr29clN  40853  cdlemefr32fvaN  40855  cdlemefr32fva1  40856  cdlemefs32sn1aw  40860  cdleme43fsv1snlem  40866  cdleme41sn3a  40879  cdleme32fva  40883  cdleme32b  40888  cdleme32d  40890  cdleme32e  40891  cdleme32f  40892  cdleme32le  40893  cdleme35a  40894  cdleme35fnpq  40895  cdleme35b  40896  cdleme35c  40897  cdleme35d  40898  cdleme35e  40899  cdleme35f  40900  cdleme36a  40906  cdleme36m  40907  cdleme37m  40908  cdleme39a  40911  cdleme39n  40912  cdleme40m  40913  cdleme40n  40914  cdleme42e  40925  cdleme42f  40926  cdleme42g  40927  cdleme43bN  40936  cdleme43cN  40937  cdleme43dN  40938  cdleme46f2g2  40939  cdleme46f2g1  40940  cdleme17d2  40941  cdleme48b  40949  cdleme4gfv  40953  cdlemeg49le  40957  cdlemeg46c  40959  cdlemeg46fvaw  40962  cdlemeg46nlpq  40963  cdlemeg46frv  40971  cdlemeg46rgv  40974  cdlemeg46req  40975  cdlemeg46gfre  40978  cdleme50trn1  40995  cdleme50trn2a  40996  cdleme50trn2  40997  cdleme  41006  cdlemf  41009  trlord  41015  cdlemg2ce  41038  cdlemg7fvbwN  41053  cdlemg7aN  41071  cdlemg10bALTN  41082  cdlemg10a  41086  cdlemg10  41087  cdlemg12d  41092  cdlemg12f  41094  cdlemg12g  41095  cdlemg12  41096  cdlemg13a  41097  cdlemg13  41098  cdlemg17b  41108  cdlemg17dN  41109  cdlemg17dALTN  41110  cdlemg17e  41111  cdlemg17f  41112  cdlemg17g  41113  cdlemg17h  41114  cdlemg17i  41115  cdlemg17pq  41118  cdlemg17bq  41119  cdlemg17iqN  41120  cdlemg17  41123  cdlemg18d  41127  cdlemg18  41128  cdlemg19a  41129  cdlemg19  41130  cdlemg21  41132  cdlemg27a  41138  cdlemg28a  41139  cdlemg31b0N  41140  cdlemg27b  41142  cdlemg33b0  41147  cdlemg28b  41149  cdlemg28  41150  cdlemg33a  41152  cdlemg33  41157  cdlemg34  41158  cdlemg35  41159  cdlemg36  41160  ltrnco  41165  trlcone  41174  cdlemg44  41179  cdlemg47  41182  cdlemg48  41183  tendococl  41218  tendoplcl  41227  cdlemh1  41261  cdlemi  41266  cdlemj1  41267  cdlemj2  41268  tendocan  41270  cdlemk6  41283  cdlemki  41287  cdlemksat  41292  cdlemksv2  41293  cdlemk7  41294  cdlemk11  41295  cdlemk12  41296  cdlemkoatnle  41297  cdlemkole  41299  cdlemk14  41300  cdlemk15  41301  cdlemk16a  41302  cdlemk16  41303  cdlemk17  41304  cdlemk1u  41305  cdlemk5u  41307  cdlemk6u  41308  cdlemkuat  41312  cdlemk18  41314  cdlemk19  41315  cdlemk12u  41318  cdlemk21N  41319  cdlemk20  41320  cdlemkoatnle-2N  41321  cdlemk13-2N  41322  cdlemkole-2N  41323  cdlemk14-2N  41324  cdlemk15-2N  41325  cdlemk16-2N  41326  cdlemk17-2N  41327  cdlemk18-2N  41332  cdlemk19-2N  41333  cdlemk7u-2N  41334  cdlemk11u-2N  41335  cdlemk12u-2N  41336  cdlemk21-2N  41337  cdlemk20-2N  41338  cdlemk22  41339  cdlemk23-3  41348  cdlemk25-3  41350  cdlemk26b-3  41351  cdlemk27-3  41353  cdlemk28-3  41354  cdlemk33N  41355  cdlemk37  41360  cdlemky  41372  cdlemk11ta  41375  cdlemkid3N  41379  cdlemk11tc  41391  cdlemk11t  41392  cdlemk45  41393  cdlemk46  41394  cdlemk47  41395  cdlemk48  41396  cdlemk49  41397  cdlemk50  41398  cdlemk51  41399  cdlemk52  41400  cdlemk55b  41406  cdlemkyyN  41408  cdlemk55u1  41411  cdlemk55u  41412  cdlemk39u1  41413  cdlemk39u  41414  cdlemk56  41417  cdleml3N  41424  cdleml4N  41425  cdlemm10N  41564  dihord1  41664  dihord2a  41665  dihord2b  41666  dihord10  41669  dihord11c  41670  dihord2pre  41671  dihord4  41704  dihord5apre  41708  dihmeetlem1N  41736  dihglbcpreN  41746  dihjatc1  41757  dihjatc3  41759  dihmeetlem13N  41765  dihmeetlem20N  41772  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  hdmap14lem11  42324  hdmap14lem12  42325  flt4lem5  43083  monotuz  43369  congmul  43395  congsub  43398  rpnnen3lem  43459  ntrclsiso  44494  ntrclskb  44496  ntrclsk3  44497  wessf1ornlem  45615  infleinf  45801  lincdifsn  48900  itsclc0yqe  49237  itsclc0xyqsolr  49245  iscnrm3rlem8  49422  iscnrm3llem2  49425