Theorem simp13 1205

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 398  df-3an 1089

This theorem is referenced by:  simp113  1304  simp213  1313  simp313  1322  omeu  8447  ackbij1lem16  10037  dvdsgcd  16297  coprimeprodsq  16554  pythagtriplem4  16565  pythagtriplem13  16573  pythagtriplem14  16574  pythagtriplem16  16576  pythagtrip  16580  lsmpropd  19328  matsc  21644  mdetunilem7  21812  smadiadetglem2  21866  m2cpminvid  21947  pmatcollpw1lem1  21968  mp2pm2mplem2  22001  isfil2  23052  filuni  23081  ufprim  23105  cxple2a  25899  isosctr  26016  brbtwn2  27318  colinearalg  27323  ax5seg  27351  axcontlem4  27380  measres  32235  bayesth  32451  nolesgn2o  33919  nogesgn1o  33921  sslttr  34046  cofcut2  34136  ofscom  34354  btwndiff  34374  ifscgr  34391  brofs2  34424  brifs2  34425  fscgr  34427  btwnconn1lem1  34434  btwnconn1lem2  34435  btwnconn1lem3  34436  btwnconn1lem4  34437  btwnconn1lem12  34445  seglecgr12im  34457  seglecgr12  34458  ivthALT  34569  islshpcv  37109  eqlkr  37155  lshpsmreu  37165  lshpkrlem5  37170  atlrelat1  37377  cvlcvr1  37395  cvlcvrp  37396  cvlatcvr1  37397  cvlatcvr2  37398  4noncolr3  37509  4noncolr2  37510  4noncolr1  37511  athgt  37512  3dimlem2  37515  3dimlem3a  37516  3dimlem4a  37519  3dimlem4  37520  3dimlem4OLDN  37521  3dim1  37523  3dim2  37524  hlatexch4  37537  ps-2b  37538  3atlem6  37544  llnnleat  37569  2atm  37583  ps-2c  37584  llnmlplnN  37595  2atmat  37617  2llnjN  37623  lvoli2  37637  4atlem3b  37654  4atlem10  37662  4atlem11a  37663  4atlem11b  37664  4atlem12a  37666  4atlem12b  37667  dalemswapyz  37712  lneq2at  37834  2lnat  37840  cdlema1N  37847  cdlemb  37850  pmodlem1  37902  llnmod2i2  37919  dalawlem1  37927  dalawlem3  37929  dalawlem4  37930  dalawlem6  37932  dalawlem9  37935  dalawlem10  37936  dalawlem11  37937  dalawlem12  37938  dalawlem13  37939  dalawlem15  37941  dalaw  37942  pclfinN  37956  osumcllem5N  38016  osumcllem6N  38017  osumcllem7N  38018  osumcllem9N  38020  osumcllem11N  38022  pl42lem1N  38035  lhp2at0  38088  lhp2atne  38090  lhp2at0ne  38092  4atexlem7  38131  ldilco  38172  ltrneq  38205  cdlemd2  38255  cdleme0ex2N  38280  cdleme7aa  38298  cdleme7c  38301  cdleme7d  38302  cdleme7ga  38304  cdleme11c  38317  cdleme11l  38325  cdleme11  38326  cdleme14  38329  cdleme15a  38330  cdleme15c  38332  cdleme16b  38335  cdleme16c  38336  cdleme16d  38337  cdleme16e  38338  cdleme16f  38339  cdleme0nex  38346  cdleme19b  38360  cdleme19d  38362  cdleme19e  38363  cdleme20f  38370  cdleme20k  38375  cdleme20l1  38376  cdleme20l2  38377  cdleme20l  38378  cdleme20m  38379  cdleme21a  38381  cdleme21b  38382  cdleme21c  38383  cdleme21ct  38385  cdleme21d  38386  cdleme21e  38387  cdleme21f  38388  cdleme21i  38391  cdleme22cN  38398  cdleme22eALTN  38401  cdleme25a  38409  cdleme25c  38411  cdleme25dN  38412  cdleme26e  38415  cdleme26ee  38416  cdleme26eALTN  38417  cdleme26f2ALTN  38420  cdleme26f2  38421  cdleme28a  38426  cdleme28b  38427  cdleme28  38429  cdlemefr32sn2aw  38460  cdlemefs32sn1aw  38470  cdleme43fsv1snlem  38476  cdleme41sn3a  38489  cdleme32c  38499  cdleme32e  38501  cdleme32le  38503  cdleme35a  38504  cdleme35b  38506  cdleme35d  38508  cdleme36a  38516  cdleme36m  38517  cdleme39a  38521  cdleme40m  38523  cdleme40n  38524  cdleme43bN  38546  cdleme43dN  38548  cdleme46f2g2  38549  cdleme46f2g1  38550  cdleme4gfv  38563  cdlemeg49le  38567  cdlemeg46c  38569  cdlemeg46fvaw  38572  cdlemeg46nlpq  38573  cdlemeg46gfre  38588  cdleme50trn2  38607  cdlemg2ce  38648  cdlemg2idN  38652  cdlemg7fvbwN  38663  cdlemg10bALTN  38692  cdlemg10a  38696  cdlemg12d  38702  cdlemg12g  38705  cdlemg12  38706  cdlemg13a  38707  cdlemg13  38708  cdlemg17b  38718  cdlemg17dN  38719  cdlemg17dALTN  38720  cdlemg17e  38721  cdlemg17pq  38728  cdlemg17bq  38729  cdlemg18d  38737  cdlemg19a  38739  cdlemg19  38740  cdlemg21  38742  cdlemg27a  38748  cdlemg31b0N  38750  cdlemg27b  38752  cdlemg31c  38755  cdlemg33b0  38757  cdlemg33c0  38758  cdlemg28b  38759  cdlemg33a  38762  cdlemg33  38767  ltrnco  38775  cdlemg44  38789  cdlemg47  38792  tendococl  38828  tendoplcl  38837  cdlemh1  38871  cdlemh2  38872  cdlemh  38873  cdlemi  38876  cdlemk5  38892  cdlemk6  38893  cdlemksel  38901  cdlemksv2  38903  cdlemk7  38904  cdlemk11  38905  cdlemk12  38906  cdlemkole  38909  cdlemk14  38910  cdlemk15  38911  cdlemk16a  38912  cdlemk16  38913  cdlemk1u  38915  cdlemk5u  38917  cdlemk6u  38918  cdlemkuel  38921  cdlemkuv2  38923  cdlemk18  38924  cdlemk19  38925  cdlemk7u  38926  cdlemk11u  38927  cdlemk12u  38928  cdlemk21N  38929  cdlemk20  38930  cdlemkoatnle-2N  38931  cdlemk13-2N  38932  cdlemkole-2N  38933  cdlemk14-2N  38934  cdlemk15-2N  38935  cdlemk16-2N  38936  cdlemk17-2N  38937  cdlemk18-2N  38942  cdlemk19-2N  38943  cdlemk7u-2N  38944  cdlemk11u-2N  38945  cdlemk12u-2N  38946  cdlemk21-2N  38947  cdlemk20-2N  38948  cdlemkuel-3  38954  cdlemkuv2-3N  38955  cdlemk22-3  38957  cdlemk33N  38965  cdlemk47  39005  cdlemk48  39006  cdlemk49  39007  cdlemk50  39008  cdlemk51  39009  cdlemk52  39010  cdlemk53a  39011  cdlemk55b  39016  cdlemkyyN  39018  cdlemk55u1  39021  cdlemk39u1  39023  cdlemk56  39027  dihord1  39274  dihord2a  39275  dihord10  39279  dihord11c  39280  dihord4  39314  dihord5apre  39318  dihglblem2N  39350  dihglbcpreN  39356  dihmeetlem3N  39361  dihjatc1  39367  dihjatc2N  39368  dihjatc3  39369  mapdpglem24  39760  baerlem3lem2  39766  baerlem5alem2  39767  baerlem5blem2  39768  hdmap14lem11  39934  hdmap14lem12  39935  hdmapglem7  39985  mzpsubst  40607  congmul  40827  congsub  40830  ntrclsiso  41715  ntrclskb  41717  ntrclsk3  41718  limsupre  43231  0ellimcdiv  43239  limclner  43241  sge0xaddlem2  44022  lincdifsn  45823  itschlc0yqe  46164  itscnhlc0xyqsol  46169