Theorem simp13 1207

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

Syntax hints:   → wi 4   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  simp113  1306  simp213  1315  simp313  1324  omeu  8313  ackbij1lem16  9849  dvdsgcd  16104  coprimeprodsq  16361  pythagtriplem4  16372  pythagtriplem13  16380  pythagtriplem14  16381  pythagtriplem16  16383  pythagtrip  16387  lsmpropd  19067  matsc  21347  mdetunilem7  21515  smadiadetglem2  21569  m2cpminvid  21650  pmatcollpw1lem1  21671  mp2pm2mplem2  21704  isfil2  22753  filuni  22782  ufprim  22806  cxple2a  25587  isosctr  25704  brbtwn2  26996  colinearalg  27001  ax5seg  27029  axcontlem4  27058  measres  31902  bayesth  32118  nolesgn2o  33611  nogesgn1o  33613  sslttr  33738  cofcut2  33828  ofscom  34046  btwndiff  34066  ifscgr  34083  brofs2  34116  brifs2  34117  fscgr  34119  btwnconn1lem1  34126  btwnconn1lem2  34127  btwnconn1lem3  34128  btwnconn1lem4  34129  btwnconn1lem12  34137  seglecgr12im  34149  seglecgr12  34150  ivthALT  34261  islshpcv  36804  eqlkr  36850  lshpsmreu  36860  lshpkrlem5  36865  atlrelat1  37072  cvlcvr1  37090  cvlcvrp  37091  cvlatcvr1  37092  cvlatcvr2  37093  4noncolr3  37204  4noncolr2  37205  4noncolr1  37206  athgt  37207  3dimlem2  37210  3dimlem3a  37211  3dimlem4a  37214  3dimlem4  37215  3dimlem4OLDN  37216  3dim1  37218  3dim2  37219  hlatexch4  37232  ps-2b  37233  3atlem6  37239  llnnleat  37264  2atm  37278  ps-2c  37279  llnmlplnN  37290  2atmat  37312  2llnjN  37318  lvoli2  37332  4atlem3b  37349  4atlem10  37357  4atlem11a  37358  4atlem11b  37359  4atlem12a  37361  4atlem12b  37362  dalemswapyz  37407  lneq2at  37529  2lnat  37535  cdlema1N  37542  cdlemb  37545  pmodlem1  37597  llnmod2i2  37614  dalawlem1  37622  dalawlem3  37624  dalawlem4  37625  dalawlem6  37627  dalawlem9  37630  dalawlem10  37631  dalawlem11  37632  dalawlem12  37633  dalawlem13  37634  dalawlem15  37636  dalaw  37637  pclfinN  37651  osumcllem5N  37711  osumcllem6N  37712  osumcllem7N  37713  osumcllem9N  37715  osumcllem11N  37717  pl42lem1N  37730  lhp2at0  37783  lhp2atne  37785  lhp2at0ne  37787  4atexlem7  37826  ldilco  37867  ltrneq  37900  cdlemd2  37950  cdleme0ex2N  37975  cdleme7aa  37993  cdleme7c  37996  cdleme7d  37997  cdleme7ga  37999  cdleme11c  38012  cdleme11l  38020  cdleme11  38021  cdleme14  38024  cdleme15a  38025  cdleme15c  38027  cdleme16b  38030  cdleme16c  38031  cdleme16d  38032  cdleme16e  38033  cdleme16f  38034  cdleme0nex  38041  cdleme19b  38055  cdleme19d  38057  cdleme19e  38058  cdleme20f  38065  cdleme20k  38070  cdleme20l1  38071  cdleme20l2  38072  cdleme20l  38073  cdleme20m  38074  cdleme21a  38076  cdleme21b  38077  cdleme21c  38078  cdleme21ct  38080  cdleme21d  38081  cdleme21e  38082  cdleme21f  38083  cdleme21i  38086  cdleme22cN  38093  cdleme22eALTN  38096  cdleme25a  38104  cdleme25c  38106  cdleme25dN  38107  cdleme26e  38110  cdleme26ee  38111  cdleme26eALTN  38112  cdleme26f2ALTN  38115  cdleme26f2  38116  cdleme28a  38121  cdleme28b  38122  cdleme28  38124  cdlemefr32sn2aw  38155  cdlemefs32sn1aw  38165  cdleme43fsv1snlem  38171  cdleme41sn3a  38184  cdleme32c  38194  cdleme32e  38196  cdleme32le  38198  cdleme35a  38199  cdleme35b  38201  cdleme35d  38203  cdleme36a  38211  cdleme36m  38212  cdleme39a  38216  cdleme40m  38218  cdleme40n  38219  cdleme43bN  38241  cdleme43dN  38243  cdleme46f2g2  38244  cdleme46f2g1  38245  cdleme4gfv  38258  cdlemeg49le  38262  cdlemeg46c  38264  cdlemeg46fvaw  38267  cdlemeg46nlpq  38268  cdlemeg46gfre  38283  cdleme50trn2  38302  cdlemg2ce  38343  cdlemg2idN  38347  cdlemg7fvbwN  38358  cdlemg10bALTN  38387  cdlemg10a  38391  cdlemg12d  38397  cdlemg12g  38400  cdlemg12  38401  cdlemg13a  38402  cdlemg13  38403  cdlemg17b  38413  cdlemg17dN  38414  cdlemg17dALTN  38415  cdlemg17e  38416  cdlemg17pq  38423  cdlemg17bq  38424  cdlemg18d  38432  cdlemg19a  38434  cdlemg19  38435  cdlemg21  38437  cdlemg27a  38443  cdlemg31b0N  38445  cdlemg27b  38447  cdlemg31c  38450  cdlemg33b0  38452  cdlemg33c0  38453  cdlemg28b  38454  cdlemg33a  38457  cdlemg33  38462  ltrnco  38470  cdlemg44  38484  cdlemg47  38487  tendococl  38523  tendoplcl  38532  cdlemh1  38566  cdlemh2  38567  cdlemh  38568  cdlemi  38571  cdlemk5  38587  cdlemk6  38588  cdlemksel  38596  cdlemksv2  38598  cdlemk7  38599  cdlemk11  38600  cdlemk12  38601  cdlemkole  38604  cdlemk14  38605  cdlemk15  38606  cdlemk16a  38607  cdlemk16  38608  cdlemk1u  38610  cdlemk5u  38612  cdlemk6u  38613  cdlemkuel  38616  cdlemkuv2  38618  cdlemk18  38619  cdlemk19  38620  cdlemk7u  38621  cdlemk11u  38622  cdlemk12u  38623  cdlemk21N  38624  cdlemk20  38625  cdlemkoatnle-2N  38626  cdlemk13-2N  38627  cdlemkole-2N  38628  cdlemk14-2N  38629  cdlemk15-2N  38630  cdlemk16-2N  38631  cdlemk17-2N  38632  cdlemk18-2N  38637  cdlemk19-2N  38638  cdlemk7u-2N  38639  cdlemk11u-2N  38640  cdlemk12u-2N  38641  cdlemk21-2N  38642  cdlemk20-2N  38643  cdlemkuel-3  38649  cdlemkuv2-3N  38650  cdlemk22-3  38652  cdlemk33N  38660  cdlemk47  38700  cdlemk48  38701  cdlemk49  38702  cdlemk50  38703  cdlemk51  38704  cdlemk52  38705  cdlemk53a  38706  cdlemk55b  38711  cdlemkyyN  38713  cdlemk55u1  38716  cdlemk39u1  38718  cdlemk56  38722  dihord1  38969  dihord2a  38970  dihord10  38974  dihord11c  38975  dihord4  39009  dihord5apre  39013  dihglblem2N  39045  dihglbcpreN  39051  dihmeetlem3N  39056  dihjatc1  39062  dihjatc2N  39063  dihjatc3  39064  mapdpglem24  39455  baerlem3lem2  39461  baerlem5alem2  39462  baerlem5blem2  39463  hdmap14lem11  39629  hdmap14lem12  39630  hdmapglem7  39680  mzpsubst  40273  congmul  40492  congsub  40495  ntrclsiso  41354  ntrclskb  41356  ntrclsk3  41357  limsupre  42857  0ellimcdiv  42865  limclner  42867  sge0xaddlem2  43647  lincdifsn  45438  itschlc0yqe  45779  itscnhlc0xyqsol  45784