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  8621  omeu  8624  ackbij1lem16  10342  coprimeprodsq  17018  pythagtriplem14  17038  pythagtrip  17044  mrelatglb  18766  subglsm  19920  lsmpropd  19924  mdetmul  22971  decpmatid  23121  isfil2  24208  filuni  24237  cxple2a  27060  isosctr  27182  flt4lem5  28013  nolesgn2o  28061  nolesgn2ores  28062  nogesgn1o  28063  nogesgn1ores  28064  nolt02o  28085  nogt01o  28086  sltstr  28206  cofcut2  28341  brbtwn2  29516  colinearalg  29521  ax5seglem3  29542  clwwlknonex2  30733  measres  34938  bayesth  35154  ofscom  36963  btwndiff  36983  ifscgr  37000  brofs2  37033  brifs2  37034  fscgr  37036  btwnconn1lem1  37043  btwnconn1lem2  37044  btwnconn1lem3  37045  btwnconn1lem4  37046  btwnconn1lem5  37047  btwnconn1lem6  37048  btwnconn1lem7  37049  btwnconn1lem8  37050  btwnconn1lem9  37051  btwnconn1lem10  37052  btwnconn1lem11  37053  btwnconn1lem12  37054  seglecgr12im  37066  seglecgr12  37067  ivthALT  37314  eqlkr  40359  lkrshp  40365  lshpkrlem5  40374  cvrval3  40673  4noncolr3  40713  4noncolr2  40714  4noncolr1  40715  athgt  40716  3dimlem2  40719  3dimlem3a  40720  3dimlem4a  40723  3dimlem4  40724  3dimlem4OLDN  40725  3dim2  40728  1cvratex  40733  hlatexch4  40741  ps-2b  40742  3atlem1  40743  3atlem2  40744  3atlem4  40746  3atlem5  40747  3atlem6  40748  llnnleat  40773  2atm  40787  ps-2c  40788  llnmlplnN  40799  lplnnlelln  40803  2atmat  40821  2llnjN  40827  lvoli2  40841  lvolnlelln  40844  4atlem3b  40858  4atlem9  40863  4atlem10a  40864  4atlem10  40866  4atlem11a  40867  4atlem11b  40868  4atlem12a  40870  4atlem12b  40871  4at  40873  4at2  40874  lplncvrlvol2  40875  2lplnj  40880  dalemswapyz  40916  dath2  40997  lneq2at  41038  2lnat  41044  cdlema1N  41051  cdlemb  41054  paddasslem15  41094  pmodlem1  41106  llnmod2i2  41123  llnexchb2lem  41128  llnexchb2  41129  dalawlem1  41131  dalawlem3  41133  dalawlem4  41134  dalawlem5  41135  dalawlem6  41136  dalawlem7  41137  dalawlem8  41138  dalawlem9  41139  dalawlem10  41140  dalawlem11  41141  dalawlem12  41142  dalawlem13  41143  dalawlem15  41145  dalaw  41146  osumcllem5N  41220  osumcllem6N  41221  osumcllem7N  41222  osumcllem9N  41224  osumcllem10N  41225  osumcllem11N  41226  pl42lem1N  41239  lhpexle3lem  41271  lhpmcvr5N  41287  lhp2atne  41294  lhp2at0ne  41296  4atexlemswapqr  41323  4atexlemex6  41334  ldilco  41376  ltrneq  41409  trlval2  41423  trlnidat  41433  cdlemd2  41459  cdlemd7  41464  cdlemd8  41465  cdleme7aa  41502  cdleme7c  41505  cdleme7d  41506  cdleme7e  41507  cdleme7ga  41508  cdleme7  41509  cdleme11c  41521  cdleme11e  41523  cdleme11l  41529  cdleme11  41530  cdleme14  41533  cdleme15a  41534  cdleme15c  41536  cdleme16b  41539  cdleme16c  41540  cdleme16d  41541  cdleme16e  41542  cdleme16f  41543  cdleme0nex  41550  cdleme18d  41555  cdleme19b  41564  cdleme19d  41566  cdleme19e  41567  cdleme20f  41574  cdleme20i  41577  cdleme20k  41579  cdleme20l1  41580  cdleme20l2  41581  cdleme20l  41582  cdleme20m  41583  cdleme21a  41585  cdleme21b  41586  cdleme21ct  41589  cdleme21d  41590  cdleme21e  41591  cdleme21f  41592  cdleme21h  41594  cdleme22eALTN  41605  cdleme22f2  41607  cdleme22g  41608  cdleme26e  41619  cdleme26eALTN  41621  cdleme26fALTN  41622  cdleme26f  41623  cdleme26f2ALTN  41624  cdleme26f2  41625  cdleme28a  41630  cdleme28b  41631  cdleme28  41633  cdleme29ex  41634  cdleme29c  41636  cdlemefrs29cpre1  41658  cdlemefr29exN  41662  cdlemefr32sn2aw  41664  cdlemefr29bpre0N  41666  cdlemefr29clN  41667  cdlemefr32fvaN  41669  cdlemefr32fva1  41670  cdlemefs32sn1aw  41674  cdleme43fsv1snlem  41680  cdleme41sn3a  41693  cdleme32fva  41697  cdleme32b  41702  cdleme32d  41704  cdleme32e  41705  cdleme32f  41706  cdleme32le  41707  cdleme35a  41708  cdleme35fnpq  41709  cdleme35b  41710  cdleme35c  41711  cdleme35d  41712  cdleme35e  41713  cdleme35f  41714  cdleme36a  41720  cdleme36m  41721  cdleme37m  41722  cdleme39a  41725  cdleme39n  41726  cdleme40m  41727  cdleme40n  41728  cdleme42e  41739  cdleme42f  41740  cdleme42g  41741  cdleme43bN  41750  cdleme43cN  41751  cdleme43dN  41752  cdleme46f2g2  41753  cdleme46f2g1  41754  cdleme17d2  41755  cdleme48b  41763  cdleme4gfv  41767  cdlemeg49le  41771  cdlemeg46c  41773  cdlemeg46fvaw  41776  cdlemeg46nlpq  41777  cdlemeg46frv  41785  cdlemeg46rgv  41788  cdlemeg46req  41789  cdlemeg46gfre  41792  cdleme50trn1  41809  cdleme50trn2a  41810  cdleme50trn2  41811  cdleme  41820  cdlemf  41823  trlord  41829  cdlemg2ce  41852  cdlemg7fvbwN  41867  cdlemg7aN  41885  cdlemg10bALTN  41896  cdlemg10a  41900  cdlemg10  41901  cdlemg12d  41906  cdlemg12f  41908  cdlemg12g  41909  cdlemg12  41910  cdlemg13a  41911  cdlemg13  41912  cdlemg17b  41922  cdlemg17dN  41923  cdlemg17dALTN  41924  cdlemg17e  41925  cdlemg17f  41926  cdlemg17g  41927  cdlemg17h  41928  cdlemg17i  41929  cdlemg17pq  41932  cdlemg17bq  41933  cdlemg17iqN  41934  cdlemg17  41937  cdlemg18d  41941  cdlemg18  41942  cdlemg19a  41943  cdlemg19  41944  cdlemg21  41946  cdlemg27a  41952  cdlemg28a  41953  cdlemg31b0N  41954  cdlemg27b  41956  cdlemg33b0  41961  cdlemg28b  41963  cdlemg28  41964  cdlemg33a  41966  cdlemg33  41971  cdlemg34  41972  cdlemg35  41973  cdlemg36  41974  ltrnco  41979  trlcone  41988  cdlemg44  41993  cdlemg47  41996  cdlemg48  41997  tendococl  42032  tendoplcl  42041  cdlemh1  42075  cdlemi  42080  cdlemj1  42081  cdlemj2  42082  tendocan  42084  cdlemk6  42097  cdlemki  42101  cdlemksat  42106  cdlemksv2  42107  cdlemk7  42108  cdlemk11  42109  cdlemk12  42110  cdlemkoatnle  42111  cdlemkole  42113  cdlemk14  42114  cdlemk15  42115  cdlemk16a  42116  cdlemk16  42117  cdlemk17  42118  cdlemk1u  42119  cdlemk5u  42121  cdlemk6u  42122  cdlemkuat  42126  cdlemk18  42128  cdlemk19  42129  cdlemk12u  42132  cdlemk21N  42133  cdlemk20  42134  cdlemkoatnle-2N  42135  cdlemk13-2N  42136  cdlemkole-2N  42137  cdlemk14-2N  42138  cdlemk15-2N  42139  cdlemk16-2N  42140  cdlemk17-2N  42141  cdlemk18-2N  42146  cdlemk19-2N  42147  cdlemk7u-2N  42148  cdlemk11u-2N  42149  cdlemk12u-2N  42150  cdlemk21-2N  42151  cdlemk20-2N  42152  cdlemk22  42153  cdlemk23-3  42162  cdlemk25-3  42164  cdlemk26b-3  42165  cdlemk27-3  42167  cdlemk28-3  42168  cdlemk33N  42169  cdlemk37  42174  cdlemky  42186  cdlemk11ta  42189  cdlemkid3N  42193  cdlemk11tc  42205  cdlemk11t  42206  cdlemk45  42207  cdlemk46  42208  cdlemk47  42209  cdlemk48  42210  cdlemk49  42211  cdlemk50  42212  cdlemk51  42213  cdlemk52  42214  cdlemk55b  42220  cdlemkyyN  42222  cdlemk55u1  42225  cdlemk55u  42226  cdlemk39u1  42227  cdlemk39u  42228  cdlemk56  42231  cdleml3N  42238  cdleml4N  42239  cdlemm10N  42378  dihord1  42478  dihord2a  42479  dihord2b  42480  dihord10  42483  dihord11c  42484  dihord2pre  42485  dihord4  42518  dihord5apre  42522  dihmeetlem1N  42550  dihglbcpreN  42560  dihjatc1  42571  dihjatc3  42573  dihmeetlem13N  42579  dihmeetlem20N  42586  baerlem3lem2  42970  baerlem5alem2  42971  baerlem5blem2  42972  hdmap14lem11  43138  hdmap14lem12  43139  monotuz  44152  congmul  44178  congsub  44181  rpnnen3lem  44242  ntrclsiso  45270  ntrclskb  45272  ntrclsk3  45273  dmstructnn  46130  wessf1ornlem  46415  infleinf  46598  lincdifsn  49751  itsclc0yqe  50088  itsclc0xyqsolr  50096  iscnrm3rlem8  50276  iscnrm3llem2  50279