Theorem simp13 1202

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp13	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒)

Proof of Theorem simp13

Step	Hyp	Ref	Expression
1		simp3 1135	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant1 1130	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  simp113  1301  simp213  1310  simp313  1319  omeu  8623  ackbij1lem16  10284  dvdsgcd  16566  coprimeprodsq  16831  pythagtriplem4  16842  pythagtriplem13  16850  pythagtriplem14  16851  pythagtriplem16  16853  pythagtrip  16857  lsmpropd  19697  matsc  22466  mdetunilem7  22634  smadiadetglem2  22688  m2cpminvid  22769  pmatcollpw1lem1  22790  mp2pm2mplem2  22823  isfil2  23874  filuni  23903  ufprim  23927  cxple2a  26749  isosctr  26872  nolesgn2o  27724  nogesgn1o  27726  sslttr  27860  cofcut2  27962  brbtwn2  28862  colinearalg  28867  ax5seg  28895  axcontlem4  28924  measres  34093  bayesth  34311  ofscom  35878  btwndiff  35898  ifscgr  35915  brofs2  35948  brifs2  35949  fscgr  35951  btwnconn1lem1  35958  btwnconn1lem2  35959  btwnconn1lem3  35960  btwnconn1lem4  35961  btwnconn1lem12  35969  seglecgr12im  35981  seglecgr12  35982  ivthALT  36095  islshpcv  38798  eqlkr  38844  lshpsmreu  38854  lshpkrlem5  38859  atlrelat1  39066  cvlcvr1  39084  cvlcvrp  39085  cvlatcvr1  39086  cvlatcvr2  39087  4noncolr3  39199  4noncolr2  39200  4noncolr1  39201  athgt  39202  3dimlem2  39205  3dimlem3a  39206  3dimlem4a  39209  3dimlem4  39210  3dimlem4OLDN  39211  3dim1  39213  3dim2  39214  hlatexch4  39227  ps-2b  39228  3atlem6  39234  llnnleat  39259  2atm  39273  ps-2c  39274  llnmlplnN  39285  2atmat  39307  2llnjN  39313  lvoli2  39327  4atlem3b  39344  4atlem10  39352  4atlem11a  39353  4atlem11b  39354  4atlem12a  39356  4atlem12b  39357  dalemswapyz  39402  lneq2at  39524  2lnat  39530  cdlema1N  39537  cdlemb  39540  pmodlem1  39592  llnmod2i2  39609  dalawlem1  39617  dalawlem3  39619  dalawlem4  39620  dalawlem6  39622  dalawlem9  39625  dalawlem10  39626  dalawlem11  39627  dalawlem12  39628  dalawlem13  39629  dalawlem15  39631  dalaw  39632  pclfinN  39646  osumcllem5N  39706  osumcllem6N  39707  osumcllem7N  39708  osumcllem9N  39710  osumcllem11N  39712  pl42lem1N  39725  lhp2at0  39778  lhp2atne  39780  lhp2at0ne  39782  4atexlem7  39821  ldilco  39862  ltrneq  39895  cdlemd2  39945  cdleme0ex2N  39970  cdleme7aa  39988  cdleme7c  39991  cdleme7d  39992  cdleme7ga  39994  cdleme11c  40007  cdleme11l  40015  cdleme11  40016  cdleme14  40019  cdleme15a  40020  cdleme15c  40022  cdleme16b  40025  cdleme16c  40026  cdleme16d  40027  cdleme16e  40028  cdleme16f  40029  cdleme0nex  40036  cdleme19b  40050  cdleme19d  40052  cdleme19e  40053  cdleme20f  40060  cdleme20k  40065  cdleme20l1  40066  cdleme20l2  40067  cdleme20l  40068  cdleme20m  40069  cdleme21a  40071  cdleme21b  40072  cdleme21c  40073  cdleme21ct  40075  cdleme21d  40076  cdleme21e  40077  cdleme21f  40078  cdleme21i  40081  cdleme22cN  40088  cdleme22eALTN  40091  cdleme25a  40099  cdleme25c  40101  cdleme25dN  40102  cdleme26e  40105  cdleme26ee  40106  cdleme26eALTN  40107  cdleme26f2ALTN  40110  cdleme26f2  40111  cdleme28a  40116  cdleme28b  40117  cdleme28  40119  cdlemefr32sn2aw  40150  cdlemefs32sn1aw  40160  cdleme43fsv1snlem  40166  cdleme41sn3a  40179  cdleme32c  40189  cdleme32e  40191  cdleme32le  40193  cdleme35a  40194  cdleme35b  40196  cdleme35d  40198  cdleme36a  40206  cdleme36m  40207  cdleme39a  40211  cdleme40m  40213  cdleme40n  40214  cdleme43bN  40236  cdleme43dN  40238  cdleme46f2g2  40239  cdleme46f2g1  40240  cdleme4gfv  40253  cdlemeg49le  40257  cdlemeg46c  40259  cdlemeg46fvaw  40262  cdlemeg46nlpq  40263  cdlemeg46gfre  40278  cdleme50trn2  40297  cdlemg2ce  40338  cdlemg2idN  40342  cdlemg7fvbwN  40353  cdlemg10bALTN  40382  cdlemg10a  40386  cdlemg12d  40392  cdlemg12g  40395  cdlemg12  40396  cdlemg13a  40397  cdlemg13  40398  cdlemg17b  40408  cdlemg17dN  40409  cdlemg17dALTN  40410  cdlemg17e  40411  cdlemg17pq  40418  cdlemg17bq  40419  cdlemg18d  40427  cdlemg19a  40429  cdlemg19  40430  cdlemg21  40432  cdlemg27a  40438  cdlemg31b0N  40440  cdlemg27b  40442  cdlemg31c  40445  cdlemg33b0  40447  cdlemg33c0  40448  cdlemg28b  40449  cdlemg33a  40452  cdlemg33  40457  ltrnco  40465  cdlemg44  40479  cdlemg47  40482  tendococl  40518  tendoplcl  40527  cdlemh1  40561  cdlemh2  40562  cdlemh  40563  cdlemi  40566  cdlemk5  40582  cdlemk6  40583  cdlemksel  40591  cdlemksv2  40593  cdlemk7  40594  cdlemk11  40595  cdlemk12  40596  cdlemkole  40599  cdlemk14  40600  cdlemk15  40601  cdlemk16a  40602  cdlemk16  40603  cdlemk1u  40605  cdlemk5u  40607  cdlemk6u  40608  cdlemkuel  40611  cdlemkuv2  40613  cdlemk18  40614  cdlemk19  40615  cdlemk7u  40616  cdlemk11u  40617  cdlemk12u  40618  cdlemk21N  40619  cdlemk20  40620  cdlemkoatnle-2N  40621  cdlemk13-2N  40622  cdlemkole-2N  40623  cdlemk14-2N  40624  cdlemk15-2N  40625  cdlemk16-2N  40626  cdlemk17-2N  40627  cdlemk18-2N  40632  cdlemk19-2N  40633  cdlemk7u-2N  40634  cdlemk11u-2N  40635  cdlemk12u-2N  40636  cdlemk21-2N  40637  cdlemk20-2N  40638  cdlemkuel-3  40644  cdlemkuv2-3N  40645  cdlemk22-3  40647  cdlemk33N  40655  cdlemk47  40695  cdlemk48  40696  cdlemk49  40697  cdlemk50  40698  cdlemk51  40699  cdlemk52  40700  cdlemk53a  40701  cdlemk55b  40706  cdlemkyyN  40708  cdlemk55u1  40711  cdlemk39u1  40713  cdlemk56  40717  dihord1  40964  dihord2a  40965  dihord10  40969  dihord11c  40970  dihord4  41004  dihord5apre  41008  dihglblem2N  41040  dihglbcpreN  41046  dihmeetlem3N  41051  dihjatc1  41057  dihjatc2N  41058  dihjatc3  41059  mapdpglem24  41450  baerlem3lem2  41456  baerlem5alem2  41457  baerlem5blem2  41458  hdmap14lem11  41624  hdmap14lem12  41625  hdmapglem7  41675  mzpsubst  42476  congmul  42696  congsub  42699  ntrclsiso  43805  ntrclskb  43807  ntrclsk3  43808  limsupre  45332  0ellimcdiv  45340  limclner  45342  sge0xaddlem2  46125  lincdifsn  47888  itschlc0yqe  48229  itscnhlc0xyqsol  48234