Theorem simp11 1216

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simp111  1315  simp211  1324  simp311  1333  omeulem1  8546  omeu  8549  ackbij1lem16  10187  coprimeprodsq  16827  pythagtriplem14  16847  pythagtrip  16853  mrelatglb  18575  subglsm  19696  lsmpropd  19700  mdetmul  22663  decpmatid  22810  isfil2  23896  filuni  23925  cxple2a  26741  isosctr  26863  nolesgn2o  27712  nolesgn2ores  27713  nogesgn1o  27714  nogesgn1ores  27715  nolt02o  27736  nogt01o  27737  sltstr  27857  cofcut2  27992  brbtwn2  29052  colinearalg  29057  ax5seglem3  29078  clwwlknonex2  30257  measres  34480  bayesth  34697  ofscom  36321  btwndiff  36341  ifscgr  36358  brofs2  36391  brifs2  36392  fscgr  36394  btwnconn1lem1  36401  btwnconn1lem2  36402  btwnconn1lem3  36403  btwnconn1lem4  36404  btwnconn1lem5  36405  btwnconn1lem6  36406  btwnconn1lem7  36407  btwnconn1lem8  36408  btwnconn1lem9  36409  btwnconn1lem10  36410  btwnconn1lem11  36411  btwnconn1lem12  36412  seglecgr12im  36424  seglecgr12  36425  ivthALT  36659  eqlkr  39687  lkrshp  39693  lshpkrlem5  39702  cvrval3  40001  4noncolr3  40041  4noncolr2  40042  4noncolr1  40043  athgt  40044  3dimlem2  40047  3dimlem3a  40048  3dimlem4a  40051  3dimlem4  40052  3dimlem4OLDN  40053  3dim2  40056  1cvratex  40061  hlatexch4  40069  ps-2b  40070  3atlem1  40071  3atlem2  40072  3atlem4  40074  3atlem5  40075  3atlem6  40076  llnnleat  40101  2atm  40115  ps-2c  40116  llnmlplnN  40127  lplnnlelln  40131  2atmat  40149  2llnjN  40155  lvoli2  40169  lvolnlelln  40172  4atlem3b  40186  4atlem9  40191  4atlem10a  40192  4atlem10  40194  4atlem11a  40195  4atlem11b  40196  4atlem12a  40198  4atlem12b  40199  4at  40201  4at2  40202  lplncvrlvol2  40203  2lplnj  40208  dalemswapyz  40244  dath2  40325  lneq2at  40366  2lnat  40372  cdlema1N  40379  cdlemb  40382  paddasslem15  40422  pmodlem1  40434  llnmod2i2  40451  llnexchb2lem  40456  llnexchb2  40457  dalawlem1  40459  dalawlem3  40461  dalawlem4  40462  dalawlem5  40463  dalawlem6  40464  dalawlem7  40465  dalawlem8  40466  dalawlem9  40467  dalawlem10  40468  dalawlem11  40469  dalawlem12  40470  dalawlem13  40471  dalawlem15  40473  dalaw  40474  osumcllem5N  40548  osumcllem6N  40549  osumcllem7N  40550  osumcllem9N  40552  osumcllem10N  40553  osumcllem11N  40554  pl42lem1N  40567  lhpexle3lem  40599  lhpmcvr5N  40615  lhp2atne  40622  lhp2at0ne  40624  4atexlemswapqr  40651  4atexlemex6  40662  ldilco  40704  ltrneq  40737  trlval2  40751  trlnidat  40761  cdlemd2  40787  cdlemd7  40792  cdlemd8  40793  cdleme7aa  40830  cdleme7c  40833  cdleme7d  40834  cdleme7e  40835  cdleme7ga  40836  cdleme7  40837  cdleme11c  40849  cdleme11e  40851  cdleme11l  40857  cdleme11  40858  cdleme14  40861  cdleme15a  40862  cdleme15c  40864  cdleme16b  40867  cdleme16c  40868  cdleme16d  40869  cdleme16e  40870  cdleme16f  40871  cdleme0nex  40878  cdleme18d  40883  cdleme19b  40892  cdleme19d  40894  cdleme19e  40895  cdleme20f  40902  cdleme20i  40905  cdleme20k  40907  cdleme20l1  40908  cdleme20l2  40909  cdleme20l  40910  cdleme20m  40911  cdleme21a  40913  cdleme21b  40914  cdleme21ct  40917  cdleme21d  40918  cdleme21e  40919  cdleme21f  40920  cdleme21h  40922  cdleme22eALTN  40933  cdleme22f2  40935  cdleme22g  40936  cdleme26e  40947  cdleme26eALTN  40949  cdleme26fALTN  40950  cdleme26f  40951  cdleme26f2ALTN  40952  cdleme26f2  40953  cdleme28a  40958  cdleme28b  40959  cdleme28  40961  cdleme29ex  40962  cdleme29c  40964  cdlemefrs29cpre1  40986  cdlemefr29exN  40990  cdlemefr32sn2aw  40992  cdlemefr29bpre0N  40994  cdlemefr29clN  40995  cdlemefr32fvaN  40997  cdlemefr32fva1  40998  cdlemefs32sn1aw  41002  cdleme43fsv1snlem  41008  cdleme41sn3a  41021  cdleme32fva  41025  cdleme32b  41030  cdleme32d  41032  cdleme32e  41033  cdleme32f  41034  cdleme32le  41035  cdleme35a  41036  cdleme35fnpq  41037  cdleme35b  41038  cdleme35c  41039  cdleme35d  41040  cdleme35e  41041  cdleme35f  41042  cdleme36a  41048  cdleme36m  41049  cdleme37m  41050  cdleme39a  41053  cdleme39n  41054  cdleme40m  41055  cdleme40n  41056  cdleme42e  41067  cdleme42f  41068  cdleme42g  41069  cdleme43bN  41078  cdleme43cN  41079  cdleme43dN  41080  cdleme46f2g2  41081  cdleme46f2g1  41082  cdleme17d2  41083  cdleme48b  41091  cdleme4gfv  41095  cdlemeg49le  41099  cdlemeg46c  41101  cdlemeg46fvaw  41104  cdlemeg46nlpq  41105  cdlemeg46frv  41113  cdlemeg46rgv  41116  cdlemeg46req  41117  cdlemeg46gfre  41120  cdleme50trn1  41137  cdleme50trn2a  41138  cdleme50trn2  41139  cdleme  41148  cdlemf  41151  trlord  41157  cdlemg2ce  41180  cdlemg7fvbwN  41195  cdlemg7aN  41213  cdlemg10bALTN  41224  cdlemg10a  41228  cdlemg10  41229  cdlemg12d  41234  cdlemg12f  41236  cdlemg12g  41237  cdlemg12  41238  cdlemg13a  41239  cdlemg13  41240  cdlemg17b  41250  cdlemg17dN  41251  cdlemg17dALTN  41252  cdlemg17e  41253  cdlemg17f  41254  cdlemg17g  41255  cdlemg17h  41256  cdlemg17i  41257  cdlemg17pq  41260  cdlemg17bq  41261  cdlemg17iqN  41262  cdlemg17  41265  cdlemg18d  41269  cdlemg18  41270  cdlemg19a  41271  cdlemg19  41272  cdlemg21  41274  cdlemg27a  41280  cdlemg28a  41281  cdlemg31b0N  41282  cdlemg27b  41284  cdlemg33b0  41289  cdlemg28b  41291  cdlemg28  41292  cdlemg33a  41294  cdlemg33  41299  cdlemg34  41300  cdlemg35  41301  cdlemg36  41302  ltrnco  41307  trlcone  41316  cdlemg44  41321  cdlemg47  41324  cdlemg48  41325  tendococl  41360  tendoplcl  41369  cdlemh1  41403  cdlemi  41408  cdlemj1  41409  cdlemj2  41410  tendocan  41412  cdlemk6  41425  cdlemki  41429  cdlemksat  41434  cdlemksv2  41435  cdlemk7  41436  cdlemk11  41437  cdlemk12  41438  cdlemkoatnle  41439  cdlemkole  41441  cdlemk14  41442  cdlemk15  41443  cdlemk16a  41444  cdlemk16  41445  cdlemk17  41446  cdlemk1u  41447  cdlemk5u  41449  cdlemk6u  41450  cdlemkuat  41454  cdlemk18  41456  cdlemk19  41457  cdlemk12u  41460  cdlemk21N  41461  cdlemk20  41462  cdlemkoatnle-2N  41463  cdlemk13-2N  41464  cdlemkole-2N  41465  cdlemk14-2N  41466  cdlemk15-2N  41467  cdlemk16-2N  41468  cdlemk17-2N  41469  cdlemk18-2N  41474  cdlemk19-2N  41475  cdlemk7u-2N  41476  cdlemk11u-2N  41477  cdlemk12u-2N  41478  cdlemk21-2N  41479  cdlemk20-2N  41480  cdlemk22  41481  cdlemk23-3  41490  cdlemk25-3  41492  cdlemk26b-3  41493  cdlemk27-3  41495  cdlemk28-3  41496  cdlemk33N  41497  cdlemk37  41502  cdlemky  41514  cdlemk11ta  41517  cdlemkid3N  41521  cdlemk11tc  41533  cdlemk11t  41534  cdlemk45  41535  cdlemk46  41536  cdlemk47  41537  cdlemk48  41538  cdlemk49  41539  cdlemk50  41540  cdlemk51  41541  cdlemk52  41542  cdlemk55b  41548  cdlemkyyN  41550  cdlemk55u1  41553  cdlemk55u  41554  cdlemk39u1  41555  cdlemk39u  41556  cdlemk56  41559  cdleml3N  41566  cdleml4N  41567  cdlemm10N  41706  dihord1  41806  dihord2a  41807  dihord2b  41808  dihord10  41811  dihord11c  41812  dihord2pre  41813  dihord4  41846  dihord5apre  41850  dihmeetlem1N  41878  dihglbcpreN  41888  dihjatc1  41899  dihjatc3  41901  dihmeetlem13N  41907  dihmeetlem20N  41914  baerlem3lem2  42298  baerlem5alem2  42299  baerlem5blem2  42300  hdmap14lem11  42466  hdmap14lem12  42467  flt4lem5  43196  monotuz  43482  congmul  43508  congsub  43511  rpnnen3lem  43572  ntrclsiso  44607  ntrclskb  44609  ntrclsk3  44610  wessf1ornlem  45727  infleinf  45911  lincdifsn  49010  itsclc0yqe  49347  itsclc0xyqsolr  49355  iscnrm3rlem8  49532  iscnrm3llem2  49535