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  8509  omeu  8512  ackbij1lem16  10144  coprimeprodsq  16736  pythagtriplem14  16756  pythagtrip  16762  mrelatglb  18483  subglsm  19602  lsmpropd  19606  mdetmul  22567  decpmatid  22714  isfil2  23800  filuni  23829  cxple2a  26664  isosctr  26787  nolesgn2o  27639  nolesgn2ores  27640  nogesgn1o  27641  nogesgn1ores  27642  nolt02o  27663  nogt01o  27664  sltstr  27783  cofcut2  27918  brbtwn2  28978  colinearalg  28983  ax5seglem3  29004  clwwlknonex2  30184  measres  34379  bayesth  34596  ofscom  36201  btwndiff  36221  ifscgr  36238  brofs2  36271  brifs2  36272  fscgr  36274  btwnconn1lem1  36281  btwnconn1lem2  36282  btwnconn1lem3  36283  btwnconn1lem4  36284  btwnconn1lem5  36285  btwnconn1lem6  36286  btwnconn1lem7  36287  btwnconn1lem8  36288  btwnconn1lem9  36289  btwnconn1lem10  36290  btwnconn1lem11  36291  btwnconn1lem12  36292  seglecgr12im  36304  seglecgr12  36305  ivthALT  36529  eqlkr  39359  lkrshp  39365  lshpkrlem5  39374  cvrval3  39673  4noncolr3  39713  4noncolr2  39714  4noncolr1  39715  athgt  39716  3dimlem2  39719  3dimlem3a  39720  3dimlem4a  39723  3dimlem4  39724  3dimlem4OLDN  39725  3dim2  39728  1cvratex  39733  hlatexch4  39741  ps-2b  39742  3atlem1  39743  3atlem2  39744  3atlem4  39746  3atlem5  39747  3atlem6  39748  llnnleat  39773  2atm  39787  ps-2c  39788  llnmlplnN  39799  lplnnlelln  39803  2atmat  39821  2llnjN  39827  lvoli2  39841  lvolnlelln  39844  4atlem3b  39858  4atlem9  39863  4atlem10a  39864  4atlem10  39866  4atlem11a  39867  4atlem11b  39868  4atlem12a  39870  4atlem12b  39871  4at  39873  4at2  39874  lplncvrlvol2  39875  2lplnj  39880  dalemswapyz  39916  dath2  39997  lneq2at  40038  2lnat  40044  cdlema1N  40051  cdlemb  40054  paddasslem15  40094  pmodlem1  40106  llnmod2i2  40123  llnexchb2lem  40128  llnexchb2  40129  dalawlem1  40131  dalawlem3  40133  dalawlem4  40134  dalawlem5  40135  dalawlem6  40136  dalawlem7  40137  dalawlem8  40138  dalawlem9  40139  dalawlem10  40140  dalawlem11  40141  dalawlem12  40142  dalawlem13  40143  dalawlem15  40145  dalaw  40146  osumcllem5N  40220  osumcllem6N  40221  osumcllem7N  40222  osumcllem9N  40224  osumcllem10N  40225  osumcllem11N  40226  pl42lem1N  40239  lhpexle3lem  40271  lhpmcvr5N  40287  lhp2atne  40294  lhp2at0ne  40296  4atexlemswapqr  40323  4atexlemex6  40334  ldilco  40376  ltrneq  40409  trlval2  40423  trlnidat  40433  cdlemd2  40459  cdlemd7  40464  cdlemd8  40465  cdleme7aa  40502  cdleme7c  40505  cdleme7d  40506  cdleme7e  40507  cdleme7ga  40508  cdleme7  40509  cdleme11c  40521  cdleme11e  40523  cdleme11l  40529  cdleme11  40530  cdleme14  40533  cdleme15a  40534  cdleme15c  40536  cdleme16b  40539  cdleme16c  40540  cdleme16d  40541  cdleme16e  40542  cdleme16f  40543  cdleme0nex  40550  cdleme18d  40555  cdleme19b  40564  cdleme19d  40566  cdleme19e  40567  cdleme20f  40574  cdleme20i  40577  cdleme20k  40579  cdleme20l1  40580  cdleme20l2  40581  cdleme20l  40582  cdleme20m  40583  cdleme21a  40585  cdleme21b  40586  cdleme21ct  40589  cdleme21d  40590  cdleme21e  40591  cdleme21f  40592  cdleme21h  40594  cdleme22eALTN  40605  cdleme22f2  40607  cdleme22g  40608  cdleme26e  40619  cdleme26eALTN  40621  cdleme26fALTN  40622  cdleme26f  40623  cdleme26f2ALTN  40624  cdleme26f2  40625  cdleme28a  40630  cdleme28b  40631  cdleme28  40633  cdleme29ex  40634  cdleme29c  40636  cdlemefrs29cpre1  40658  cdlemefr29exN  40662  cdlemefr32sn2aw  40664  cdlemefr29bpre0N  40666  cdlemefr29clN  40667  cdlemefr32fvaN  40669  cdlemefr32fva1  40670  cdlemefs32sn1aw  40674  cdleme43fsv1snlem  40680  cdleme41sn3a  40693  cdleme32fva  40697  cdleme32b  40702  cdleme32d  40704  cdleme32e  40705  cdleme32f  40706  cdleme32le  40707  cdleme35a  40708  cdleme35fnpq  40709  cdleme35b  40710  cdleme35c  40711  cdleme35d  40712  cdleme35e  40713  cdleme35f  40714  cdleme36a  40720  cdleme36m  40721  cdleme37m  40722  cdleme39a  40725  cdleme39n  40726  cdleme40m  40727  cdleme40n  40728  cdleme42e  40739  cdleme42f  40740  cdleme42g  40741  cdleme43bN  40750  cdleme43cN  40751  cdleme43dN  40752  cdleme46f2g2  40753  cdleme46f2g1  40754  cdleme17d2  40755  cdleme48b  40763  cdleme4gfv  40767  cdlemeg49le  40771  cdlemeg46c  40773  cdlemeg46fvaw  40776  cdlemeg46nlpq  40777  cdlemeg46frv  40785  cdlemeg46rgv  40788  cdlemeg46req  40789  cdlemeg46gfre  40792  cdleme50trn1  40809  cdleme50trn2a  40810  cdleme50trn2  40811  cdleme  40820  cdlemf  40823  trlord  40829  cdlemg2ce  40852  cdlemg7fvbwN  40867  cdlemg7aN  40885  cdlemg10bALTN  40896  cdlemg10a  40900  cdlemg10  40901  cdlemg12d  40906  cdlemg12f  40908  cdlemg12g  40909  cdlemg12  40910  cdlemg13a  40911  cdlemg13  40912  cdlemg17b  40922  cdlemg17dN  40923  cdlemg17dALTN  40924  cdlemg17e  40925  cdlemg17f  40926  cdlemg17g  40927  cdlemg17h  40928  cdlemg17i  40929  cdlemg17pq  40932  cdlemg17bq  40933  cdlemg17iqN  40934  cdlemg17  40937  cdlemg18d  40941  cdlemg18  40942  cdlemg19a  40943  cdlemg19  40944  cdlemg21  40946  cdlemg27a  40952  cdlemg28a  40953  cdlemg31b0N  40954  cdlemg27b  40956  cdlemg33b0  40961  cdlemg28b  40963  cdlemg28  40964  cdlemg33a  40966  cdlemg33  40971  cdlemg34  40972  cdlemg35  40973  cdlemg36  40974  ltrnco  40979  trlcone  40988  cdlemg44  40993  cdlemg47  40996  cdlemg48  40997  tendococl  41032  tendoplcl  41041  cdlemh1  41075  cdlemi  41080  cdlemj1  41081  cdlemj2  41082  tendocan  41084  cdlemk6  41097  cdlemki  41101  cdlemksat  41106  cdlemksv2  41107  cdlemk7  41108  cdlemk11  41109  cdlemk12  41110  cdlemkoatnle  41111  cdlemkole  41113  cdlemk14  41114  cdlemk15  41115  cdlemk16a  41116  cdlemk16  41117  cdlemk17  41118  cdlemk1u  41119  cdlemk5u  41121  cdlemk6u  41122  cdlemkuat  41126  cdlemk18  41128  cdlemk19  41129  cdlemk12u  41132  cdlemk21N  41133  cdlemk20  41134  cdlemkoatnle-2N  41135  cdlemk13-2N  41136  cdlemkole-2N  41137  cdlemk14-2N  41138  cdlemk15-2N  41139  cdlemk16-2N  41140  cdlemk17-2N  41141  cdlemk18-2N  41146  cdlemk19-2N  41147  cdlemk7u-2N  41148  cdlemk11u-2N  41149  cdlemk12u-2N  41150  cdlemk21-2N  41151  cdlemk20-2N  41152  cdlemk22  41153  cdlemk23-3  41162  cdlemk25-3  41164  cdlemk26b-3  41165  cdlemk27-3  41167  cdlemk28-3  41168  cdlemk33N  41169  cdlemk37  41174  cdlemky  41186  cdlemk11ta  41189  cdlemkid3N  41193  cdlemk11tc  41205  cdlemk11t  41206  cdlemk45  41207  cdlemk46  41208  cdlemk47  41209  cdlemk48  41210  cdlemk49  41211  cdlemk50  41212  cdlemk51  41213  cdlemk52  41214  cdlemk55b  41220  cdlemkyyN  41222  cdlemk55u1  41225  cdlemk55u  41226  cdlemk39u1  41227  cdlemk39u  41228  cdlemk56  41231  cdleml3N  41238  cdleml4N  41239  cdlemm10N  41378  dihord1  41478  dihord2a  41479  dihord2b  41480  dihord10  41483  dihord11c  41484  dihord2pre  41485  dihord4  41518  dihord5apre  41522  dihmeetlem1N  41550  dihglbcpreN  41560  dihjatc1  41571  dihjatc3  41573  dihmeetlem13N  41579  dihmeetlem20N  41586  baerlem3lem2  41970  baerlem5alem2  41971  baerlem5blem2  41972  hdmap14lem11  42138  hdmap14lem12  42139  flt4lem5  42893  monotuz  43183  congmul  43209  congsub  43212  rpnnen3lem  43273  ntrclsiso  44308  ntrclskb  44310  ntrclsk3  44311  wessf1ornlem  45429  infleinf  45616  lincdifsn  48670  itsclc0yqe  49007  itsclc0xyqsolr  49015  iscnrm3rlem8  49192  iscnrm3llem2  49195