Theorem simp13 1204

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 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant1 1132	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  simp113  1303  simp213  1312  simp313  1321  omeu  8591  ackbij1lem16  10236  dvdsgcd  16493  coprimeprodsq  16748  pythagtriplem4  16759  pythagtriplem13  16767  pythagtriplem14  16768  pythagtriplem16  16770  pythagtrip  16774  lsmpropd  19593  matsc  22272  mdetunilem7  22440  smadiadetglem2  22494  m2cpminvid  22575  pmatcollpw1lem1  22596  mp2pm2mplem2  22629  isfil2  23680  filuni  23709  ufprim  23733  cxple2a  26547  isosctr  26667  nolesgn2o  27517  nogesgn1o  27519  sslttr  27653  cofcut2  27755  brbtwn2  28596  colinearalg  28601  ax5seg  28629  axcontlem4  28658  measres  33684  bayesth  33902  ofscom  35449  btwndiff  35469  ifscgr  35486  brofs2  35519  brifs2  35520  fscgr  35522  btwnconn1lem1  35529  btwnconn1lem2  35530  btwnconn1lem3  35531  btwnconn1lem4  35532  btwnconn1lem12  35540  seglecgr12im  35552  seglecgr12  35553  ivthALT  35684  islshpcv  38387  eqlkr  38433  lshpsmreu  38443  lshpkrlem5  38448  atlrelat1  38655  cvlcvr1  38673  cvlcvrp  38674  cvlatcvr1  38675  cvlatcvr2  38676  4noncolr3  38788  4noncolr2  38789  4noncolr1  38790  athgt  38791  3dimlem2  38794  3dimlem3a  38795  3dimlem4a  38798  3dimlem4  38799  3dimlem4OLDN  38800  3dim1  38802  3dim2  38803  hlatexch4  38816  ps-2b  38817  3atlem6  38823  llnnleat  38848  2atm  38862  ps-2c  38863  llnmlplnN  38874  2atmat  38896  2llnjN  38902  lvoli2  38916  4atlem3b  38933  4atlem10  38941  4atlem11a  38942  4atlem11b  38943  4atlem12a  38945  4atlem12b  38946  dalemswapyz  38991  lneq2at  39113  2lnat  39119  cdlema1N  39126  cdlemb  39129  pmodlem1  39181  llnmod2i2  39198  dalawlem1  39206  dalawlem3  39208  dalawlem4  39209  dalawlem6  39211  dalawlem9  39214  dalawlem10  39215  dalawlem11  39216  dalawlem12  39217  dalawlem13  39218  dalawlem15  39220  dalaw  39221  pclfinN  39235  osumcllem5N  39295  osumcllem6N  39296  osumcllem7N  39297  osumcllem9N  39299  osumcllem11N  39301  pl42lem1N  39314  lhp2at0  39367  lhp2atne  39369  lhp2at0ne  39371  4atexlem7  39410  ldilco  39451  ltrneq  39484  cdlemd2  39534  cdleme0ex2N  39559  cdleme7aa  39577  cdleme7c  39580  cdleme7d  39581  cdleme7ga  39583  cdleme11c  39596  cdleme11l  39604  cdleme11  39605  cdleme14  39608  cdleme15a  39609  cdleme15c  39611  cdleme16b  39614  cdleme16c  39615  cdleme16d  39616  cdleme16e  39617  cdleme16f  39618  cdleme0nex  39625  cdleme19b  39639  cdleme19d  39641  cdleme19e  39642  cdleme20f  39649  cdleme20k  39654  cdleme20l1  39655  cdleme20l2  39656  cdleme20l  39657  cdleme20m  39658  cdleme21a  39660  cdleme21b  39661  cdleme21c  39662  cdleme21ct  39664  cdleme21d  39665  cdleme21e  39666  cdleme21f  39667  cdleme21i  39670  cdleme22cN  39677  cdleme22eALTN  39680  cdleme25a  39688  cdleme25c  39690  cdleme25dN  39691  cdleme26e  39694  cdleme26ee  39695  cdleme26eALTN  39696  cdleme26f2ALTN  39699  cdleme26f2  39700  cdleme28a  39705  cdleme28b  39706  cdleme28  39708  cdlemefr32sn2aw  39739  cdlemefs32sn1aw  39749  cdleme43fsv1snlem  39755  cdleme41sn3a  39768  cdleme32c  39778  cdleme32e  39780  cdleme32le  39782  cdleme35a  39783  cdleme35b  39785  cdleme35d  39787  cdleme36a  39795  cdleme36m  39796  cdleme39a  39800  cdleme40m  39802  cdleme40n  39803  cdleme43bN  39825  cdleme43dN  39827  cdleme46f2g2  39828  cdleme46f2g1  39829  cdleme4gfv  39842  cdlemeg49le  39846  cdlemeg46c  39848  cdlemeg46fvaw  39851  cdlemeg46nlpq  39852  cdlemeg46gfre  39867  cdleme50trn2  39886  cdlemg2ce  39927  cdlemg2idN  39931  cdlemg7fvbwN  39942  cdlemg10bALTN  39971  cdlemg10a  39975  cdlemg12d  39981  cdlemg12g  39984  cdlemg12  39985  cdlemg13a  39986  cdlemg13  39987  cdlemg17b  39997  cdlemg17dN  39998  cdlemg17dALTN  39999  cdlemg17e  40000  cdlemg17pq  40007  cdlemg17bq  40008  cdlemg18d  40016  cdlemg19a  40018  cdlemg19  40019  cdlemg21  40021  cdlemg27a  40027  cdlemg31b0N  40029  cdlemg27b  40031  cdlemg31c  40034  cdlemg33b0  40036  cdlemg33c0  40037  cdlemg28b  40038  cdlemg33a  40041  cdlemg33  40046  ltrnco  40054  cdlemg44  40068  cdlemg47  40071  tendococl  40107  tendoplcl  40116  cdlemh1  40150  cdlemh2  40151  cdlemh  40152  cdlemi  40155  cdlemk5  40171  cdlemk6  40172  cdlemksel  40180  cdlemksv2  40182  cdlemk7  40183  cdlemk11  40184  cdlemk12  40185  cdlemkole  40188  cdlemk14  40189  cdlemk15  40190  cdlemk16a  40191  cdlemk16  40192  cdlemk1u  40194  cdlemk5u  40196  cdlemk6u  40197  cdlemkuel  40200  cdlemkuv2  40202  cdlemk18  40203  cdlemk19  40204  cdlemk7u  40205  cdlemk11u  40206  cdlemk12u  40207  cdlemk21N  40208  cdlemk20  40209  cdlemkoatnle-2N  40210  cdlemk13-2N  40211  cdlemkole-2N  40212  cdlemk14-2N  40213  cdlemk15-2N  40214  cdlemk16-2N  40215  cdlemk17-2N  40216  cdlemk18-2N  40221  cdlemk19-2N  40222  cdlemk7u-2N  40223  cdlemk11u-2N  40224  cdlemk12u-2N  40225  cdlemk21-2N  40226  cdlemk20-2N  40227  cdlemkuel-3  40233  cdlemkuv2-3N  40234  cdlemk22-3  40236  cdlemk33N  40244  cdlemk47  40284  cdlemk48  40285  cdlemk49  40286  cdlemk50  40287  cdlemk51  40288  cdlemk52  40289  cdlemk53a  40290  cdlemk55b  40295  cdlemkyyN  40297  cdlemk55u1  40300  cdlemk39u1  40302  cdlemk56  40306  dihord1  40553  dihord2a  40554  dihord10  40558  dihord11c  40559  dihord4  40593  dihord5apre  40597  dihglblem2N  40629  dihglbcpreN  40635  dihmeetlem3N  40640  dihjatc1  40646  dihjatc2N  40647  dihjatc3  40648  mapdpglem24  41039  baerlem3lem2  41045  baerlem5alem2  41046  baerlem5blem2  41047  hdmap14lem11  41213  hdmap14lem12  41214  hdmapglem7  41264  mzpsubst  41949  congmul  42169  congsub  42172  ntrclsiso  43281  ntrclskb  43283  ntrclsk3  43284  limsupre  44816  0ellimcdiv  44824  limclner  44826  sge0xaddlem2  45609  lincdifsn  47267  itschlc0yqe  47608  itscnhlc0xyqsol  47613