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  8546  omeu  8549  ackbij1lem16  10187  coprimeprodsq  16779  pythagtriplem14  16799  pythagtrip  16805  mrelatglb  18519  subglsm  19603  lsmpropd  19607  mdetmul  22510  decpmatid  22657  isfil2  23743  filuni  23772  cxple2a  26608  isosctr  26731  nolesgn2o  27583  nolesgn2ores  27584  nogesgn1o  27585  nogesgn1ores  27586  nolt02o  27607  nogt01o  27608  sslttr  27719  cofcut2  27830  brbtwn2  28832  colinearalg  28837  ax5seglem3  28858  clwwlknonex2  30038  measres  34212  bayesth  34430  ofscom  35995  btwndiff  36015  ifscgr  36032  brofs2  36065  brifs2  36066  fscgr  36068  btwnconn1lem1  36075  btwnconn1lem2  36076  btwnconn1lem3  36077  btwnconn1lem4  36078  btwnconn1lem5  36079  btwnconn1lem6  36080  btwnconn1lem7  36081  btwnconn1lem8  36082  btwnconn1lem9  36083  btwnconn1lem10  36084  btwnconn1lem11  36085  btwnconn1lem12  36086  seglecgr12im  36098  seglecgr12  36099  ivthALT  36323  eqlkr  39092  lkrshp  39098  lshpkrlem5  39107  cvrval3  39407  4noncolr3  39447  4noncolr2  39448  4noncolr1  39449  athgt  39450  3dimlem2  39453  3dimlem3a  39454  3dimlem4a  39457  3dimlem4  39458  3dimlem4OLDN  39459  3dim2  39462  1cvratex  39467  hlatexch4  39475  ps-2b  39476  3atlem1  39477  3atlem2  39478  3atlem4  39480  3atlem5  39481  3atlem6  39482  llnnleat  39507  2atm  39521  ps-2c  39522  llnmlplnN  39533  lplnnlelln  39537  2atmat  39555  2llnjN  39561  lvoli2  39575  lvolnlelln  39578  4atlem3b  39592  4atlem9  39597  4atlem10a  39598  4atlem10  39600  4atlem11a  39601  4atlem11b  39602  4atlem12a  39604  4atlem12b  39605  4at  39607  4at2  39608  lplncvrlvol2  39609  2lplnj  39614  dalemswapyz  39650  dath2  39731  lneq2at  39772  2lnat  39778  cdlema1N  39785  cdlemb  39788  paddasslem15  39828  pmodlem1  39840  llnmod2i2  39857  llnexchb2lem  39862  llnexchb2  39863  dalawlem1  39865  dalawlem3  39867  dalawlem4  39868  dalawlem5  39869  dalawlem6  39870  dalawlem7  39871  dalawlem8  39872  dalawlem9  39873  dalawlem10  39874  dalawlem11  39875  dalawlem12  39876  dalawlem13  39877  dalawlem15  39879  dalaw  39880  osumcllem5N  39954  osumcllem6N  39955  osumcllem7N  39956  osumcllem9N  39958  osumcllem10N  39959  osumcllem11N  39960  pl42lem1N  39973  lhpexle3lem  40005  lhpmcvr5N  40021  lhp2atne  40028  lhp2at0ne  40030  4atexlemswapqr  40057  4atexlemex6  40068  ldilco  40110  ltrneq  40143  trlval2  40157  trlnidat  40167  cdlemd2  40193  cdlemd7  40198  cdlemd8  40199  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme11c  40255  cdleme11e  40257  cdleme11l  40263  cdleme11  40264  cdleme14  40267  cdleme15a  40268  cdleme15c  40270  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme16e  40276  cdleme16f  40277  cdleme0nex  40284  cdleme18d  40289  cdleme19b  40298  cdleme19d  40300  cdleme19e  40301  cdleme20f  40308  cdleme20i  40311  cdleme20k  40313  cdleme20l1  40314  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme21a  40319  cdleme21b  40320  cdleme21ct  40323  cdleme21d  40324  cdleme21e  40325  cdleme21f  40326  cdleme21h  40328  cdleme22eALTN  40339  cdleme22f2  40341  cdleme22g  40342  cdleme26e  40353  cdleme26eALTN  40355  cdleme26fALTN  40356  cdleme26f  40357  cdleme26f2ALTN  40358  cdleme26f2  40359  cdleme28a  40364  cdleme28b  40365  cdleme28  40367  cdleme29ex  40368  cdleme29c  40370  cdlemefrs29cpre1  40392  cdlemefr29exN  40396  cdlemefr32sn2aw  40398  cdlemefr29bpre0N  40400  cdlemefr29clN  40401  cdlemefr32fvaN  40403  cdlemefr32fva1  40404  cdlemefs32sn1aw  40408  cdleme43fsv1snlem  40414  cdleme41sn3a  40427  cdleme32fva  40431  cdleme32b  40436  cdleme32d  40438  cdleme32e  40439  cdleme32f  40440  cdleme32le  40441  cdleme35a  40442  cdleme35fnpq  40443  cdleme35b  40444  cdleme35c  40445  cdleme35d  40446  cdleme35e  40447  cdleme35f  40448  cdleme36a  40454  cdleme36m  40455  cdleme37m  40456  cdleme39a  40459  cdleme39n  40460  cdleme40m  40461  cdleme40n  40462  cdleme42e  40473  cdleme42f  40474  cdleme42g  40475  cdleme43bN  40484  cdleme43cN  40485  cdleme43dN  40486  cdleme46f2g2  40487  cdleme46f2g1  40488  cdleme17d2  40489  cdleme48b  40497  cdleme4gfv  40501  cdlemeg49le  40505  cdlemeg46c  40507  cdlemeg46fvaw  40510  cdlemeg46nlpq  40511  cdlemeg46frv  40519  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemeg46gfre  40526  cdleme50trn1  40543  cdleme50trn2a  40544  cdleme50trn2  40545  cdleme  40554  cdlemf  40557  trlord  40563  cdlemg2ce  40586  cdlemg7fvbwN  40601  cdlemg7aN  40619  cdlemg10bALTN  40630  cdlemg10a  40634  cdlemg10  40635  cdlemg12d  40640  cdlemg12f  40642  cdlemg12g  40643  cdlemg12  40644  cdlemg13a  40645  cdlemg13  40646  cdlemg17b  40656  cdlemg17dN  40657  cdlemg17dALTN  40658  cdlemg17e  40659  cdlemg17f  40660  cdlemg17g  40661  cdlemg17h  40662  cdlemg17i  40663  cdlemg17pq  40666  cdlemg17bq  40667  cdlemg17iqN  40668  cdlemg17  40671  cdlemg18d  40675  cdlemg18  40676  cdlemg19a  40677  cdlemg19  40678  cdlemg21  40680  cdlemg27a  40686  cdlemg28a  40687  cdlemg31b0N  40688  cdlemg27b  40690  cdlemg33b0  40695  cdlemg28b  40697  cdlemg28  40698  cdlemg33a  40700  cdlemg33  40705  cdlemg34  40706  cdlemg35  40707  cdlemg36  40708  ltrnco  40713  trlcone  40722  cdlemg44  40727  cdlemg47  40730  cdlemg48  40731  tendococl  40766  tendoplcl  40775  cdlemh1  40809  cdlemi  40814  cdlemj1  40815  cdlemj2  40816  tendocan  40818  cdlemk6  40831  cdlemki  40835  cdlemksat  40840  cdlemksv2  40841  cdlemk7  40842  cdlemk11  40843  cdlemk12  40844  cdlemkoatnle  40845  cdlemkole  40847  cdlemk14  40848  cdlemk15  40849  cdlemk16a  40850  cdlemk16  40851  cdlemk17  40852  cdlemk1u  40853  cdlemk5u  40855  cdlemk6u  40856  cdlemkuat  40860  cdlemk18  40862  cdlemk19  40863  cdlemk12u  40866  cdlemk21N  40867  cdlemk20  40868  cdlemkoatnle-2N  40869  cdlemk13-2N  40870  cdlemkole-2N  40871  cdlemk14-2N  40872  cdlemk15-2N  40873  cdlemk16-2N  40874  cdlemk17-2N  40875  cdlemk18-2N  40880  cdlemk19-2N  40881  cdlemk7u-2N  40882  cdlemk11u-2N  40883  cdlemk12u-2N  40884  cdlemk21-2N  40885  cdlemk20-2N  40886  cdlemk22  40887  cdlemk23-3  40896  cdlemk25-3  40898  cdlemk26b-3  40899  cdlemk27-3  40901  cdlemk28-3  40902  cdlemk33N  40903  cdlemk37  40908  cdlemky  40920  cdlemk11ta  40923  cdlemkid3N  40927  cdlemk11tc  40939  cdlemk11t  40940  cdlemk45  40941  cdlemk46  40942  cdlemk47  40943  cdlemk48  40944  cdlemk49  40945  cdlemk50  40946  cdlemk51  40947  cdlemk52  40948  cdlemk55b  40954  cdlemkyyN  40956  cdlemk55u1  40959  cdlemk55u  40960  cdlemk39u1  40961  cdlemk39u  40962  cdlemk56  40965  cdleml3N  40972  cdleml4N  40973  cdlemm10N  41112  dihord1  41212  dihord2a  41213  dihord2b  41214  dihord10  41217  dihord11c  41218  dihord2pre  41219  dihord4  41252  dihord5apre  41256  dihmeetlem1N  41284  dihglbcpreN  41294  dihjatc1  41305  dihjatc3  41307  dihmeetlem13N  41313  dihmeetlem20N  41320  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  hdmap14lem11  41872  hdmap14lem12  41873  flt4lem5  42638  monotuz  42930  congmul  42956  congsub  42959  rpnnen3lem  43020  ntrclsiso  44056  ntrclskb  44058  ntrclsk3  44059  wessf1ornlem  45179  infleinf  45368  lincdifsn  48413  itsclc0yqe  48750  itsclc0xyqsolr  48758  iscnrm3rlem8  48935  iscnrm3llem2  48938