Theorem simp11 1222

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp111  1321  simp211  1330  simp311  1339  omeulem1  8573  omeu  8576  ackbij1lem16  10240  coprimeprodsq  16906  pythagtriplem14  16926  pythagtrip  16932  mrelatglb  18654  subglsm  19806  lsmpropd  19810  mdetmul  22851  decpmatid  23001  isfil2  24088  filuni  24117  cxple2a  26944  isosctr  27066  nolesgn2o  27915  nolesgn2ores  27916  nogesgn1o  27917  nogesgn1ores  27918  nolt02o  27939  nogt01o  27940  sltstr  28060  cofcut2  28195  brbtwn2  29370  colinearalg  29375  ax5seglem3  29396  clwwlknonex2  30587  measres  34741  bayesth  34958  ofscom  36595  btwndiff  36615  ifscgr  36632  brofs2  36665  brifs2  36666  fscgr  36668  btwnconn1lem1  36675  btwnconn1lem2  36676  btwnconn1lem3  36677  btwnconn1lem4  36678  btwnconn1lem5  36679  btwnconn1lem6  36680  btwnconn1lem7  36681  btwnconn1lem8  36682  btwnconn1lem9  36683  btwnconn1lem10  36684  btwnconn1lem11  36685  btwnconn1lem12  36686  seglecgr12im  36698  seglecgr12  36699  ivthALT  36962  eqlkr  39980  lkrshp  39986  lshpkrlem5  39995  cvrval3  40294  4noncolr3  40334  4noncolr2  40335  4noncolr1  40336  athgt  40337  3dimlem2  40340  3dimlem3a  40341  3dimlem4a  40344  3dimlem4  40345  3dimlem4OLDN  40346  3dim2  40349  1cvratex  40354  hlatexch4  40362  ps-2b  40363  3atlem1  40364  3atlem2  40365  3atlem4  40367  3atlem5  40368  3atlem6  40369  llnnleat  40394  2atm  40408  ps-2c  40409  llnmlplnN  40420  lplnnlelln  40424  2atmat  40442  2llnjN  40448  lvoli2  40462  lvolnlelln  40465  4atlem3b  40479  4atlem9  40484  4atlem10a  40485  4atlem10  40487  4atlem11a  40488  4atlem11b  40489  4atlem12a  40491  4atlem12b  40492  4at  40494  4at2  40495  lplncvrlvol2  40496  2lplnj  40501  dalemswapyz  40537  dath2  40618  lneq2at  40659  2lnat  40665  cdlema1N  40672  cdlemb  40675  paddasslem15  40715  pmodlem1  40727  llnmod2i2  40744  llnexchb2lem  40749  llnexchb2  40750  dalawlem1  40752  dalawlem3  40754  dalawlem4  40755  dalawlem5  40756  dalawlem6  40757  dalawlem7  40758  dalawlem8  40759  dalawlem9  40760  dalawlem10  40761  dalawlem11  40762  dalawlem12  40763  dalawlem13  40764  dalawlem15  40766  dalaw  40767  osumcllem5N  40841  osumcllem6N  40842  osumcllem7N  40843  osumcllem9N  40845  osumcllem10N  40846  osumcllem11N  40847  pl42lem1N  40860  lhpexle3lem  40892  lhpmcvr5N  40908  lhp2atne  40915  lhp2at0ne  40917  4atexlemswapqr  40944  4atexlemex6  40955  ldilco  40997  ltrneq  41030  trlval2  41044  trlnidat  41054  cdlemd2  41080  cdlemd7  41085  cdlemd8  41086  cdleme7aa  41123  cdleme7c  41126  cdleme7d  41127  cdleme7e  41128  cdleme7ga  41129  cdleme7  41130  cdleme11c  41142  cdleme11e  41144  cdleme11l  41150  cdleme11  41151  cdleme14  41154  cdleme15a  41155  cdleme15c  41157  cdleme16b  41160  cdleme16c  41161  cdleme16d  41162  cdleme16e  41163  cdleme16f  41164  cdleme0nex  41171  cdleme18d  41176  cdleme19b  41185  cdleme19d  41187  cdleme19e  41188  cdleme20f  41195  cdleme20i  41198  cdleme20k  41200  cdleme20l1  41201  cdleme20l2  41202  cdleme20l  41203  cdleme20m  41204  cdleme21a  41206  cdleme21b  41207  cdleme21ct  41210  cdleme21d  41211  cdleme21e  41212  cdleme21f  41213  cdleme21h  41215  cdleme22eALTN  41226  cdleme22f2  41228  cdleme22g  41229  cdleme26e  41240  cdleme26eALTN  41242  cdleme26fALTN  41243  cdleme26f  41244  cdleme26f2ALTN  41245  cdleme26f2  41246  cdleme28a  41251  cdleme28b  41252  cdleme28  41254  cdleme29ex  41255  cdleme29c  41257  cdlemefrs29cpre1  41279  cdlemefr29exN  41283  cdlemefr32sn2aw  41285  cdlemefr29bpre0N  41287  cdlemefr29clN  41288  cdlemefr32fvaN  41290  cdlemefr32fva1  41291  cdlemefs32sn1aw  41295  cdleme43fsv1snlem  41301  cdleme41sn3a  41314  cdleme32fva  41318  cdleme32b  41323  cdleme32d  41325  cdleme32e  41326  cdleme32f  41327  cdleme32le  41328  cdleme35a  41329  cdleme35fnpq  41330  cdleme35b  41331  cdleme35c  41332  cdleme35d  41333  cdleme35e  41334  cdleme35f  41335  cdleme36a  41341  cdleme36m  41342  cdleme37m  41343  cdleme39a  41346  cdleme39n  41347  cdleme40m  41348  cdleme40n  41349  cdleme42e  41360  cdleme42f  41361  cdleme42g  41362  cdleme43bN  41371  cdleme43cN  41372  cdleme43dN  41373  cdleme46f2g2  41374  cdleme46f2g1  41375  cdleme17d2  41376  cdleme48b  41384  cdleme4gfv  41388  cdlemeg49le  41392  cdlemeg46c  41394  cdlemeg46fvaw  41397  cdlemeg46nlpq  41398  cdlemeg46frv  41406  cdlemeg46rgv  41409  cdlemeg46req  41410  cdlemeg46gfre  41413  cdleme50trn1  41430  cdleme50trn2a  41431  cdleme50trn2  41432  cdleme  41441  cdlemf  41444  trlord  41450  cdlemg2ce  41473  cdlemg7fvbwN  41488  cdlemg7aN  41506  cdlemg10bALTN  41517  cdlemg10a  41521  cdlemg10  41522  cdlemg12d  41527  cdlemg12f  41529  cdlemg12g  41530  cdlemg12  41531  cdlemg13a  41532  cdlemg13  41533  cdlemg17b  41543  cdlemg17dN  41544  cdlemg17dALTN  41545  cdlemg17e  41546  cdlemg17f  41547  cdlemg17g  41548  cdlemg17h  41549  cdlemg17i  41550  cdlemg17pq  41553  cdlemg17bq  41554  cdlemg17iqN  41555  cdlemg17  41558  cdlemg18d  41562  cdlemg18  41563  cdlemg19a  41564  cdlemg19  41565  cdlemg21  41567  cdlemg27a  41573  cdlemg28a  41574  cdlemg31b0N  41575  cdlemg27b  41577  cdlemg33b0  41582  cdlemg28b  41584  cdlemg28  41585  cdlemg33a  41587  cdlemg33  41592  cdlemg34  41593  cdlemg35  41594  cdlemg36  41595  ltrnco  41600  trlcone  41609  cdlemg44  41614  cdlemg47  41617  cdlemg48  41618  tendococl  41653  tendoplcl  41662  cdlemh1  41696  cdlemi  41701  cdlemj1  41702  cdlemj2  41703  tendocan  41705  cdlemk6  41718  cdlemki  41722  cdlemksat  41727  cdlemksv2  41728  cdlemk7  41729  cdlemk11  41730  cdlemk12  41731  cdlemkoatnle  41732  cdlemkole  41734  cdlemk14  41735  cdlemk15  41736  cdlemk16a  41737  cdlemk16  41738  cdlemk17  41739  cdlemk1u  41740  cdlemk5u  41742  cdlemk6u  41743  cdlemkuat  41747  cdlemk18  41749  cdlemk19  41750  cdlemk12u  41753  cdlemk21N  41754  cdlemk20  41755  cdlemkoatnle-2N  41756  cdlemk13-2N  41757  cdlemkole-2N  41758  cdlemk14-2N  41759  cdlemk15-2N  41760  cdlemk16-2N  41761  cdlemk17-2N  41762  cdlemk18-2N  41767  cdlemk19-2N  41768  cdlemk7u-2N  41769  cdlemk11u-2N  41770  cdlemk12u-2N  41771  cdlemk21-2N  41772  cdlemk20-2N  41773  cdlemk22  41774  cdlemk23-3  41783  cdlemk25-3  41785  cdlemk26b-3  41786  cdlemk27-3  41788  cdlemk28-3  41789  cdlemk33N  41790  cdlemk37  41795  cdlemky  41807  cdlemk11ta  41810  cdlemkid3N  41814  cdlemk11tc  41826  cdlemk11t  41827  cdlemk45  41828  cdlemk46  41829  cdlemk47  41830  cdlemk48  41831  cdlemk49  41832  cdlemk50  41833  cdlemk51  41834  cdlemk52  41835  cdlemk55b  41841  cdlemkyyN  41843  cdlemk55u1  41846  cdlemk55u  41847  cdlemk39u1  41848  cdlemk39u  41849  cdlemk56  41852  cdleml3N  41859  cdleml4N  41860  cdlemm10N  41999  dihord1  42099  dihord2a  42100  dihord2b  42101  dihord10  42104  dihord11c  42105  dihord2pre  42106  dihord4  42139  dihord5apre  42143  dihmeetlem1N  42171  dihglbcpreN  42181  dihjatc1  42192  dihjatc3  42194  dihmeetlem13N  42200  dihmeetlem20N  42207  baerlem3lem2  42591  baerlem5alem2  42592  baerlem5blem2  42593  hdmap14lem11  42759  hdmap14lem12  42760  flt4lem5  43504  monotuz  43790  congmul  43816  congsub  43819  rpnnen3lem  43880  ntrclsiso  44915  ntrclskb  44917  ntrclsk3  44918  wessf1ornlem  46025  infleinf  46209  lincdifsn  49362  itsclc0yqe  49699  itsclc0xyqsolr  49707  iscnrm3rlem8  49881  iscnrm3llem2  49884