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  8549  omeu  8552  ackbij1lem16  10194  coprimeprodsq  16786  pythagtriplem14  16806  pythagtrip  16812  mrelatglb  18526  subglsm  19610  lsmpropd  19614  mdetmul  22517  decpmatid  22664  isfil2  23750  filuni  23779  cxple2a  26615  isosctr  26738  nolesgn2o  27590  nolesgn2ores  27591  nogesgn1o  27592  nogesgn1ores  27593  nolt02o  27614  nogt01o  27615  sslttr  27726  cofcut2  27837  brbtwn2  28839  colinearalg  28844  ax5seglem3  28865  clwwlknonex2  30045  measres  34219  bayesth  34437  ofscom  36002  btwndiff  36022  ifscgr  36039  brofs2  36072  brifs2  36073  fscgr  36075  btwnconn1lem1  36082  btwnconn1lem2  36083  btwnconn1lem3  36084  btwnconn1lem4  36085  btwnconn1lem5  36086  btwnconn1lem6  36087  btwnconn1lem7  36088  btwnconn1lem8  36089  btwnconn1lem9  36090  btwnconn1lem10  36091  btwnconn1lem11  36092  btwnconn1lem12  36093  seglecgr12im  36105  seglecgr12  36106  ivthALT  36330  eqlkr  39099  lkrshp  39105  lshpkrlem5  39114  cvrval3  39414  4noncolr3  39454  4noncolr2  39455  4noncolr1  39456  athgt  39457  3dimlem2  39460  3dimlem3a  39461  3dimlem4a  39464  3dimlem4  39465  3dimlem4OLDN  39466  3dim2  39469  1cvratex  39474  hlatexch4  39482  ps-2b  39483  3atlem1  39484  3atlem2  39485  3atlem4  39487  3atlem5  39488  3atlem6  39489  llnnleat  39514  2atm  39528  ps-2c  39529  llnmlplnN  39540  lplnnlelln  39544  2atmat  39562  2llnjN  39568  lvoli2  39582  lvolnlelln  39585  4atlem3b  39599  4atlem9  39604  4atlem10a  39605  4atlem10  39607  4atlem11a  39608  4atlem11b  39609  4atlem12a  39611  4atlem12b  39612  4at  39614  4at2  39615  lplncvrlvol2  39616  2lplnj  39621  dalemswapyz  39657  dath2  39738  lneq2at  39779  2lnat  39785  cdlema1N  39792  cdlemb  39795  paddasslem15  39835  pmodlem1  39847  llnmod2i2  39864  llnexchb2lem  39869  llnexchb2  39870  dalawlem1  39872  dalawlem3  39874  dalawlem4  39875  dalawlem5  39876  dalawlem6  39877  dalawlem7  39878  dalawlem8  39879  dalawlem9  39880  dalawlem10  39881  dalawlem11  39882  dalawlem12  39883  dalawlem13  39884  dalawlem15  39886  dalaw  39887  osumcllem5N  39961  osumcllem6N  39962  osumcllem7N  39963  osumcllem9N  39965  osumcllem10N  39966  osumcllem11N  39967  pl42lem1N  39980  lhpexle3lem  40012  lhpmcvr5N  40028  lhp2atne  40035  lhp2at0ne  40037  4atexlemswapqr  40064  4atexlemex6  40075  ldilco  40117  ltrneq  40150  trlval2  40164  trlnidat  40174  cdlemd2  40200  cdlemd7  40205  cdlemd8  40206  cdleme7aa  40243  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme7  40250  cdleme11c  40262  cdleme11e  40264  cdleme11l  40270  cdleme11  40271  cdleme14  40274  cdleme15a  40275  cdleme15c  40277  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme16e  40283  cdleme16f  40284  cdleme0nex  40291  cdleme18d  40296  cdleme19b  40305  cdleme19d  40307  cdleme19e  40308  cdleme20f  40315  cdleme20i  40318  cdleme20k  40320  cdleme20l1  40321  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme21a  40326  cdleme21b  40327  cdleme21ct  40330  cdleme21d  40331  cdleme21e  40332  cdleme21f  40333  cdleme21h  40335  cdleme22eALTN  40346  cdleme22f2  40348  cdleme22g  40349  cdleme26e  40360  cdleme26eALTN  40362  cdleme26fALTN  40363  cdleme26f  40364  cdleme26f2ALTN  40365  cdleme26f2  40366  cdleme28a  40371  cdleme28b  40372  cdleme28  40374  cdleme29ex  40375  cdleme29c  40377  cdlemefrs29cpre1  40399  cdlemefr29exN  40403  cdlemefr32sn2aw  40405  cdlemefr29bpre0N  40407  cdlemefr29clN  40408  cdlemefr32fvaN  40410  cdlemefr32fva1  40411  cdlemefs32sn1aw  40415  cdleme43fsv1snlem  40421  cdleme41sn3a  40434  cdleme32fva  40438  cdleme32b  40443  cdleme32d  40445  cdleme32e  40446  cdleme32f  40447  cdleme32le  40448  cdleme35a  40449  cdleme35fnpq  40450  cdleme35b  40451  cdleme35c  40452  cdleme35d  40453  cdleme35e  40454  cdleme35f  40455  cdleme36a  40461  cdleme36m  40462  cdleme37m  40463  cdleme39a  40466  cdleme39n  40467  cdleme40m  40468  cdleme40n  40469  cdleme42e  40480  cdleme42f  40481  cdleme42g  40482  cdleme43bN  40491  cdleme43cN  40492  cdleme43dN  40493  cdleme46f2g2  40494  cdleme46f2g1  40495  cdleme17d2  40496  cdleme48b  40504  cdleme4gfv  40508  cdlemeg49le  40512  cdlemeg46c  40514  cdlemeg46fvaw  40517  cdlemeg46nlpq  40518  cdlemeg46frv  40526  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemeg46gfre  40533  cdleme50trn1  40550  cdleme50trn2a  40551  cdleme50trn2  40552  cdleme  40561  cdlemf  40564  trlord  40570  cdlemg2ce  40593  cdlemg7fvbwN  40608  cdlemg7aN  40626  cdlemg10bALTN  40637  cdlemg10a  40641  cdlemg10  40642  cdlemg12d  40647  cdlemg12f  40649  cdlemg12g  40650  cdlemg12  40651  cdlemg13a  40652  cdlemg13  40653  cdlemg17b  40663  cdlemg17dN  40664  cdlemg17dALTN  40665  cdlemg17e  40666  cdlemg17f  40667  cdlemg17g  40668  cdlemg17h  40669  cdlemg17i  40670  cdlemg17pq  40673  cdlemg17bq  40674  cdlemg17iqN  40675  cdlemg17  40678  cdlemg18d  40682  cdlemg18  40683  cdlemg19a  40684  cdlemg19  40685  cdlemg21  40687  cdlemg27a  40693  cdlemg28a  40694  cdlemg31b0N  40695  cdlemg27b  40697  cdlemg33b0  40702  cdlemg28b  40704  cdlemg28  40705  cdlemg33a  40707  cdlemg33  40712  cdlemg34  40713  cdlemg35  40714  cdlemg36  40715  ltrnco  40720  trlcone  40729  cdlemg44  40734  cdlemg47  40737  cdlemg48  40738  tendococl  40773  tendoplcl  40782  cdlemh1  40816  cdlemi  40821  cdlemj1  40822  cdlemj2  40823  tendocan  40825  cdlemk6  40838  cdlemki  40842  cdlemksat  40847  cdlemksv2  40848  cdlemk7  40849  cdlemk11  40850  cdlemk12  40851  cdlemkoatnle  40852  cdlemkole  40854  cdlemk14  40855  cdlemk15  40856  cdlemk16a  40857  cdlemk16  40858  cdlemk17  40859  cdlemk1u  40860  cdlemk5u  40862  cdlemk6u  40863  cdlemkuat  40867  cdlemk18  40869  cdlemk19  40870  cdlemk12u  40873  cdlemk21N  40874  cdlemk20  40875  cdlemkoatnle-2N  40876  cdlemk13-2N  40877  cdlemkole-2N  40878  cdlemk14-2N  40879  cdlemk15-2N  40880  cdlemk16-2N  40881  cdlemk17-2N  40882  cdlemk18-2N  40887  cdlemk19-2N  40888  cdlemk7u-2N  40889  cdlemk11u-2N  40890  cdlemk12u-2N  40891  cdlemk21-2N  40892  cdlemk20-2N  40893  cdlemk22  40894  cdlemk23-3  40903  cdlemk25-3  40905  cdlemk26b-3  40906  cdlemk27-3  40908  cdlemk28-3  40909  cdlemk33N  40910  cdlemk37  40915  cdlemky  40927  cdlemk11ta  40930  cdlemkid3N  40934  cdlemk11tc  40946  cdlemk11t  40947  cdlemk45  40948  cdlemk46  40949  cdlemk47  40950  cdlemk48  40951  cdlemk49  40952  cdlemk50  40953  cdlemk51  40954  cdlemk52  40955  cdlemk55b  40961  cdlemkyyN  40963  cdlemk55u1  40966  cdlemk55u  40967  cdlemk39u1  40968  cdlemk39u  40969  cdlemk56  40972  cdleml3N  40979  cdleml4N  40980  cdlemm10N  41119  dihord1  41219  dihord2a  41220  dihord2b  41221  dihord10  41224  dihord11c  41225  dihord2pre  41226  dihord4  41259  dihord5apre  41263  dihmeetlem1N  41291  dihglbcpreN  41301  dihjatc1  41312  dihjatc3  41314  dihmeetlem13N  41320  dihmeetlem20N  41327  baerlem3lem2  41711  baerlem5alem2  41712  baerlem5blem2  41713  hdmap14lem11  41879  hdmap14lem12  41880  flt4lem5  42645  monotuz  42937  congmul  42963  congsub  42966  rpnnen3lem  43027  ntrclsiso  44063  ntrclskb  44065  ntrclsk3  44066  wessf1ornlem  45186  infleinf  45375  lincdifsn  48417  itsclc0yqe  48754  itsclc0xyqsolr  48762  iscnrm3rlem8  48939  iscnrm3llem2  48942