Theorem simp13 1212

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp113  1311  simp213  1320  simp313  1329  omeu  8510  ackbij1lem16  10147  dvdsgcd  16504  coprimeprodsq  16770  pythagtriplem4  16781  pythagtriplem13  16789  pythagtriplem14  16790  pythagtriplem16  16792  pythagtrip  16796  lsmpropd  19643  matsc  22433  mdetunilem7  22601  smadiadetglem2  22655  m2cpminvid  22736  pmatcollpw1lem1  22757  mp2pm2mplem2  22790  isfil2  23839  filuni  23868  ufprim  23892  cxple2a  26681  isosctr  26803  nolesgn2o  27653  nogesgn1o  27655  sltstr  27797  cofcut2  27932  onsfi  28366  brbtwn2  28992  colinearalg  28997  ax5seg  29025  axcontlem4  29054  measres  34406  bayesth  34623  ofscom  36235  btwndiff  36255  ifscgr  36272  brofs2  36305  brifs2  36306  fscgr  36308  btwnconn1lem1  36315  btwnconn1lem2  36316  btwnconn1lem3  36317  btwnconn1lem4  36318  btwnconn1lem12  36326  seglecgr12im  36338  seglecgr12  36339  ivthALT  36563  islshpcv  39545  eqlkr  39591  lshpsmreu  39601  lshpkrlem5  39606  atlrelat1  39813  cvlcvr1  39831  cvlcvrp  39832  cvlatcvr1  39833  cvlatcvr2  39834  4noncolr3  39945  4noncolr2  39946  4noncolr1  39947  athgt  39948  3dimlem2  39951  3dimlem3a  39952  3dimlem4a  39955  3dimlem4  39956  3dimlem4OLDN  39957  3dim1  39959  3dim2  39960  hlatexch4  39973  ps-2b  39974  3atlem6  39980  llnnleat  40005  2atm  40019  ps-2c  40020  llnmlplnN  40031  2atmat  40053  2llnjN  40059  lvoli2  40073  4atlem3b  40090  4atlem10  40098  4atlem11a  40099  4atlem11b  40100  4atlem12a  40102  4atlem12b  40103  dalemswapyz  40148  lneq2at  40270  2lnat  40276  cdlema1N  40283  cdlemb  40286  pmodlem1  40338  llnmod2i2  40355  dalawlem1  40363  dalawlem3  40365  dalawlem4  40366  dalawlem6  40368  dalawlem9  40371  dalawlem10  40372  dalawlem11  40373  dalawlem12  40374  dalawlem13  40375  dalawlem15  40377  dalaw  40378  pclfinN  40392  osumcllem5N  40452  osumcllem6N  40453  osumcllem7N  40454  osumcllem9N  40456  osumcllem11N  40458  pl42lem1N  40471  lhp2at0  40524  lhp2atne  40526  lhp2at0ne  40528  4atexlem7  40567  ldilco  40608  ltrneq  40641  cdlemd2  40691  cdleme0ex2N  40716  cdleme7aa  40734  cdleme7c  40737  cdleme7d  40738  cdleme7ga  40740  cdleme11c  40753  cdleme11l  40761  cdleme11  40762  cdleme14  40765  cdleme15a  40766  cdleme15c  40768  cdleme16b  40771  cdleme16c  40772  cdleme16d  40773  cdleme16e  40774  cdleme16f  40775  cdleme0nex  40782  cdleme19b  40796  cdleme19d  40798  cdleme19e  40799  cdleme20f  40806  cdleme20k  40811  cdleme20l1  40812  cdleme20l2  40813  cdleme20l  40814  cdleme20m  40815  cdleme21a  40817  cdleme21b  40818  cdleme21c  40819  cdleme21ct  40821  cdleme21d  40822  cdleme21e  40823  cdleme21f  40824  cdleme21i  40827  cdleme22cN  40834  cdleme22eALTN  40837  cdleme25a  40845  cdleme25c  40847  cdleme25dN  40848  cdleme26e  40851  cdleme26ee  40852  cdleme26eALTN  40853  cdleme26f2ALTN  40856  cdleme26f2  40857  cdleme28a  40862  cdleme28b  40863  cdleme28  40865  cdlemefr32sn2aw  40896  cdlemefs32sn1aw  40906  cdleme43fsv1snlem  40912  cdleme41sn3a  40925  cdleme32c  40935  cdleme32e  40937  cdleme32le  40939  cdleme35a  40940  cdleme35b  40942  cdleme35d  40944  cdleme36a  40952  cdleme36m  40953  cdleme39a  40957  cdleme40m  40959  cdleme40n  40960  cdleme43bN  40982  cdleme43dN  40984  cdleme46f2g2  40985  cdleme46f2g1  40986  cdleme4gfv  40999  cdlemeg49le  41003  cdlemeg46c  41005  cdlemeg46fvaw  41008  cdlemeg46nlpq  41009  cdlemeg46gfre  41024  cdleme50trn2  41043  cdlemg2ce  41084  cdlemg2idN  41088  cdlemg7fvbwN  41099  cdlemg10bALTN  41128  cdlemg10a  41132  cdlemg12d  41138  cdlemg12g  41141  cdlemg12  41142  cdlemg13a  41143  cdlemg13  41144  cdlemg17b  41154  cdlemg17dN  41155  cdlemg17dALTN  41156  cdlemg17e  41157  cdlemg17pq  41164  cdlemg17bq  41165  cdlemg18d  41173  cdlemg19a  41175  cdlemg19  41176  cdlemg21  41178  cdlemg27a  41184  cdlemg31b0N  41186  cdlemg27b  41188  cdlemg31c  41191  cdlemg33b0  41193  cdlemg33c0  41194  cdlemg28b  41195  cdlemg33a  41198  cdlemg33  41203  ltrnco  41211  cdlemg44  41225  cdlemg47  41228  tendococl  41264  tendoplcl  41273  cdlemh1  41307  cdlemh2  41308  cdlemh  41309  cdlemi  41312  cdlemk5  41328  cdlemk6  41329  cdlemksel  41337  cdlemksv2  41339  cdlemk7  41340  cdlemk11  41341  cdlemk12  41342  cdlemkole  41345  cdlemk14  41346  cdlemk15  41347  cdlemk16a  41348  cdlemk16  41349  cdlemk1u  41351  cdlemk5u  41353  cdlemk6u  41354  cdlemkuel  41357  cdlemkuv2  41359  cdlemk18  41360  cdlemk19  41361  cdlemk7u  41362  cdlemk11u  41363  cdlemk12u  41364  cdlemk21N  41365  cdlemk20  41366  cdlemkoatnle-2N  41367  cdlemk13-2N  41368  cdlemkole-2N  41369  cdlemk14-2N  41370  cdlemk15-2N  41371  cdlemk16-2N  41372  cdlemk17-2N  41373  cdlemk18-2N  41378  cdlemk19-2N  41379  cdlemk7u-2N  41380  cdlemk11u-2N  41381  cdlemk12u-2N  41382  cdlemk21-2N  41383  cdlemk20-2N  41384  cdlemkuel-3  41390  cdlemkuv2-3N  41391  cdlemk22-3  41393  cdlemk33N  41401  cdlemk47  41441  cdlemk48  41442  cdlemk49  41443  cdlemk50  41444  cdlemk51  41445  cdlemk52  41446  cdlemk53a  41447  cdlemk55b  41452  cdlemkyyN  41454  cdlemk55u1  41457  cdlemk39u1  41459  cdlemk56  41463  dihord1  41710  dihord2a  41711  dihord10  41715  dihord11c  41716  dihord4  41750  dihord5apre  41754  dihglblem2N  41786  dihglbcpreN  41792  dihmeetlem3N  41797  dihjatc1  41803  dihjatc2N  41804  dihjatc3  41805  mapdpglem24  42196  baerlem3lem2  42202  baerlem5alem2  42203  baerlem5blem2  42204  hdmap14lem11  42370  hdmap14lem12  42371  hdmapglem7  42421  mzpsubst  43197  congmul  43412  congsub  43415  ntrclsiso  44511  ntrclskb  44513  ntrclsk3  44514  limsupre  46084  0ellimcdiv  46092  limclner  46094  sge0xaddlem2  46877  clnbgr3stgrgrlim  48510  gpgedgvtx1  48553  lincdifsn  48915  itschlc0yqe  49251  itscnhlc0xyqsol  49256