Theorem simp11 1183

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

Syntax hints:   → wi 4   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  simp111  1282  simp211  1291  simp311  1300  omeulem1  8001  omeu  8004  ackbij1lem16  9447  coprimeprodsq  15991  pythagtriplem14  16011  pythagtrip  16017  mrelatglb  17642  subglsm  18547  lsmpropd  18551  mdetmul  20926  decpmatid  21072  isfil2  22158  filuni  22187  cxple2a  24973  isosctr  25090  brbtwn2  26384  colinearalg  26389  ax5seglem3  26410  clwwlknonex2  27627  measres  31083  bayesth  31300  nolesgn2o  32639  nolesgn2ores  32640  nolt02o  32660  ofscom  32929  btwndiff  32949  ifscgr  32966  brofs2  32999  brifs2  33000  fscgr  33002  btwnconn1lem1  33009  btwnconn1lem2  33010  btwnconn1lem3  33011  btwnconn1lem4  33012  btwnconn1lem5  33013  btwnconn1lem6  33014  btwnconn1lem7  33015  btwnconn1lem8  33016  btwnconn1lem9  33017  btwnconn1lem10  33018  btwnconn1lem11  33019  btwnconn1lem12  33020  seglecgr12im  33032  seglecgr12  33033  ivthALT  33144  eqlkr  35628  lkrshp  35634  lshpkrlem5  35643  cvrval3  35942  4noncolr3  35982  4noncolr2  35983  4noncolr1  35984  athgt  35985  3dimlem2  35988  3dimlem3a  35989  3dimlem4a  35992  3dimlem4  35993  3dimlem4OLDN  35994  3dim2  35997  1cvratex  36002  hlatexch4  36010  ps-2b  36011  3atlem1  36012  3atlem2  36013  3atlem4  36015  3atlem5  36016  3atlem6  36017  llnnleat  36042  2atm  36056  ps-2c  36057  llnmlplnN  36068  lplnnlelln  36072  2atmat  36090  2llnjN  36096  lvoli2  36110  lvolnlelln  36113  4atlem3b  36127  4atlem9  36132  4atlem10a  36133  4atlem10  36135  4atlem11a  36136  4atlem11b  36137  4atlem12a  36139  4atlem12b  36140  4at  36142  4at2  36143  lplncvrlvol2  36144  2lplnj  36149  dalemswapyz  36185  dath2  36266  lneq2at  36307  2lnat  36313  cdlema1N  36320  cdlemb  36323  paddasslem15  36363  pmodlem1  36375  llnmod2i2  36392  llnexchb2lem  36397  llnexchb2  36398  dalawlem1  36400  dalawlem3  36402  dalawlem4  36403  dalawlem5  36404  dalawlem6  36405  dalawlem7  36406  dalawlem8  36407  dalawlem9  36408  dalawlem10  36409  dalawlem11  36410  dalawlem12  36411  dalawlem13  36412  dalawlem15  36414  dalaw  36415  osumcllem5N  36489  osumcllem6N  36490  osumcllem7N  36491  osumcllem9N  36493  osumcllem10N  36494  osumcllem11N  36495  pl42lem1N  36508  lhpexle3lem  36540  lhpmcvr5N  36556  lhp2atne  36563  lhp2at0ne  36565  4atexlemswapqr  36592  4atexlemex6  36603  ldilco  36645  ltrneq  36678  trlval2  36692  trlnidat  36702  cdlemd2  36728  cdlemd7  36733  cdlemd8  36734  cdleme7aa  36771  cdleme7c  36774  cdleme7d  36775  cdleme7e  36776  cdleme7ga  36777  cdleme7  36778  cdleme11c  36790  cdleme11e  36792  cdleme11l  36798  cdleme11  36799  cdleme14  36802  cdleme15a  36803  cdleme15c  36805  cdleme16b  36808  cdleme16c  36809  cdleme16d  36810  cdleme16e  36811  cdleme16f  36812  cdleme0nex  36819  cdleme18d  36824  cdleme19b  36833  cdleme19d  36835  cdleme19e  36836  cdleme20f  36843  cdleme20i  36846  cdleme20k  36848  cdleme20l1  36849  cdleme20l2  36850  cdleme20l  36851  cdleme20m  36852  cdleme21a  36854  cdleme21b  36855  cdleme21ct  36858  cdleme21d  36859  cdleme21e  36860  cdleme21f  36861  cdleme21h  36863  cdleme22eALTN  36874  cdleme22f2  36876  cdleme22g  36877  cdleme26e  36888  cdleme26eALTN  36890  cdleme26fALTN  36891  cdleme26f  36892  cdleme26f2ALTN  36893  cdleme26f2  36894  cdleme28a  36899  cdleme28b  36900  cdleme28  36902  cdleme29ex  36903  cdleme29c  36905  cdlemefrs29cpre1  36927  cdlemefr29exN  36931  cdlemefr32sn2aw  36933  cdlemefr29bpre0N  36935  cdlemefr29clN  36936  cdlemefr32fvaN  36938  cdlemefr32fva1  36939  cdlemefs32sn1aw  36943  cdleme43fsv1snlem  36949  cdleme41sn3a  36962  cdleme32fva  36966  cdleme32b  36971  cdleme32d  36973  cdleme32e  36974  cdleme32f  36975  cdleme32le  36976  cdleme35a  36977  cdleme35fnpq  36978  cdleme35b  36979  cdleme35c  36980  cdleme35d  36981  cdleme35e  36982  cdleme35f  36983  cdleme36a  36989  cdleme36m  36990  cdleme37m  36991  cdleme39a  36994  cdleme39n  36995  cdleme40m  36996  cdleme40n  36997  cdleme42e  37008  cdleme42f  37009  cdleme42g  37010  cdleme43bN  37019  cdleme43cN  37020  cdleme43dN  37021  cdleme46f2g2  37022  cdleme46f2g1  37023  cdleme17d2  37024  cdleme48b  37032  cdleme4gfv  37036  cdlemeg49le  37040  cdlemeg46c  37042  cdlemeg46fvaw  37045  cdlemeg46nlpq  37046  cdlemeg46frv  37054  cdlemeg46rgv  37057  cdlemeg46req  37058  cdlemeg46gfre  37061  cdleme50trn1  37078  cdleme50trn2a  37079  cdleme50trn2  37080  cdleme  37089  cdlemf  37092  trlord  37098  cdlemg2ce  37121  cdlemg7fvbwN  37136  cdlemg7aN  37154  cdlemg10bALTN  37165  cdlemg10a  37169  cdlemg10  37170  cdlemg12d  37175  cdlemg12f  37177  cdlemg12g  37178  cdlemg12  37179  cdlemg13a  37180  cdlemg13  37181  cdlemg17b  37191  cdlemg17dN  37192  cdlemg17dALTN  37193  cdlemg17e  37194  cdlemg17f  37195  cdlemg17g  37196  cdlemg17h  37197  cdlemg17i  37198  cdlemg17pq  37201  cdlemg17bq  37202  cdlemg17iqN  37203  cdlemg17  37206  cdlemg18d  37210  cdlemg18  37211  cdlemg19a  37212  cdlemg19  37213  cdlemg21  37215  cdlemg27a  37221  cdlemg28a  37222  cdlemg31b0N  37223  cdlemg27b  37225  cdlemg33b0  37230  cdlemg28b  37232  cdlemg28  37233  cdlemg33a  37235  cdlemg33  37240  cdlemg34  37241  cdlemg35  37242  cdlemg36  37243  ltrnco  37248  trlcone  37257  cdlemg44  37262  cdlemg47  37265  cdlemg48  37266  tendococl  37301  tendoplcl  37310  cdlemh1  37344  cdlemi  37349  cdlemj1  37350  cdlemj2  37351  tendocan  37353  cdlemk6  37366  cdlemki  37370  cdlemksat  37375  cdlemksv2  37376  cdlemk7  37377  cdlemk11  37378  cdlemk12  37379  cdlemkoatnle  37380  cdlemkole  37382  cdlemk14  37383  cdlemk15  37384  cdlemk16a  37385  cdlemk16  37386  cdlemk17  37387  cdlemk1u  37388  cdlemk5u  37390  cdlemk6u  37391  cdlemkuat  37395  cdlemk18  37397  cdlemk19  37398  cdlemk12u  37401  cdlemk21N  37402  cdlemk20  37403  cdlemkoatnle-2N  37404  cdlemk13-2N  37405  cdlemkole-2N  37406  cdlemk14-2N  37407  cdlemk15-2N  37408  cdlemk16-2N  37409  cdlemk17-2N  37410  cdlemk18-2N  37415  cdlemk19-2N  37416  cdlemk7u-2N  37417  cdlemk11u-2N  37418  cdlemk12u-2N  37419  cdlemk21-2N  37420  cdlemk20-2N  37421  cdlemk22  37422  cdlemk23-3  37431  cdlemk25-3  37433  cdlemk26b-3  37434  cdlemk27-3  37436  cdlemk28-3  37437  cdlemk33N  37438  cdlemk37  37443  cdlemky  37455  cdlemk11ta  37458  cdlemkid3N  37462  cdlemk11tc  37474  cdlemk11t  37475  cdlemk45  37476  cdlemk46  37477  cdlemk47  37478  cdlemk48  37479  cdlemk49  37480  cdlemk50  37481  cdlemk51  37482  cdlemk52  37483  cdlemk55b  37489  cdlemkyyN  37491  cdlemk55u1  37494  cdlemk55u  37495  cdlemk39u1  37496  cdlemk39u  37497  cdlemk56  37500  cdleml3N  37507  cdleml4N  37508  cdlemm10N  37647  dihord1  37747  dihord2a  37748  dihord2b  37749  dihord10  37752  dihord11c  37753  dihord2pre  37754  dihord4  37787  dihord5apre  37791  dihmeetlem1N  37819  dihglbcpreN  37829  dihjatc1  37840  dihjatc3  37842  dihmeetlem13N  37848  dihmeetlem20N  37855  baerlem3lem2  38239  baerlem5alem2  38240  baerlem5blem2  38241  hdmap14lem11  38407  hdmap14lem12  38408  monotuz  38879  congmul  38905  congsub  38908  rpnnen3lem  38969  ntrclsiso  39725  ntrclskb  39727  ntrclsk3  39728  wessf1ornlem  40815  infleinf  41015  lincdifsn  43786  itsclc0yqe  44056  itsclc0xyqsolr  44064