Theorem simp13 1206

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 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp113  1305  simp213  1314  simp313  1323  omeu  8512  ackbij1lem16  10144  dvdsgcd  16471  coprimeprodsq  16736  pythagtriplem4  16747  pythagtriplem13  16755  pythagtriplem14  16756  pythagtriplem16  16758  pythagtrip  16762  lsmpropd  19606  matsc  22394  mdetunilem7  22562  smadiadetglem2  22616  m2cpminvid  22697  pmatcollpw1lem1  22718  mp2pm2mplem2  22751  isfil2  23800  filuni  23829  ufprim  23853  cxple2a  26664  isosctr  26787  nolesgn2o  27639  nogesgn1o  27641  sltstr  27783  cofcut2  27918  onsfi  28352  brbtwn2  28978  colinearalg  28983  ax5seg  29011  axcontlem4  29040  measres  34379  bayesth  34596  ofscom  36201  btwndiff  36221  ifscgr  36238  brofs2  36271  brifs2  36272  fscgr  36274  btwnconn1lem1  36281  btwnconn1lem2  36282  btwnconn1lem3  36283  btwnconn1lem4  36284  btwnconn1lem12  36292  seglecgr12im  36304  seglecgr12  36305  ivthALT  36529  islshpcv  39313  eqlkr  39359  lshpsmreu  39369  lshpkrlem5  39374  atlrelat1  39581  cvlcvr1  39599  cvlcvrp  39600  cvlatcvr1  39601  cvlatcvr2  39602  4noncolr3  39713  4noncolr2  39714  4noncolr1  39715  athgt  39716  3dimlem2  39719  3dimlem3a  39720  3dimlem4a  39723  3dimlem4  39724  3dimlem4OLDN  39725  3dim1  39727  3dim2  39728  hlatexch4  39741  ps-2b  39742  3atlem6  39748  llnnleat  39773  2atm  39787  ps-2c  39788  llnmlplnN  39799  2atmat  39821  2llnjN  39827  lvoli2  39841  4atlem3b  39858  4atlem10  39866  4atlem11a  39867  4atlem11b  39868  4atlem12a  39870  4atlem12b  39871  dalemswapyz  39916  lneq2at  40038  2lnat  40044  cdlema1N  40051  cdlemb  40054  pmodlem1  40106  llnmod2i2  40123  dalawlem1  40131  dalawlem3  40133  dalawlem4  40134  dalawlem6  40136  dalawlem9  40139  dalawlem10  40140  dalawlem11  40141  dalawlem12  40142  dalawlem13  40143  dalawlem15  40145  dalaw  40146  pclfinN  40160  osumcllem5N  40220  osumcllem6N  40221  osumcllem7N  40222  osumcllem9N  40224  osumcllem11N  40226  pl42lem1N  40239  lhp2at0  40292  lhp2atne  40294  lhp2at0ne  40296  4atexlem7  40335  ldilco  40376  ltrneq  40409  cdlemd2  40459  cdleme0ex2N  40484  cdleme7aa  40502  cdleme7c  40505  cdleme7d  40506  cdleme7ga  40508  cdleme11c  40521  cdleme11l  40529  cdleme11  40530  cdleme14  40533  cdleme15a  40534  cdleme15c  40536  cdleme16b  40539  cdleme16c  40540  cdleme16d  40541  cdleme16e  40542  cdleme16f  40543  cdleme0nex  40550  cdleme19b  40564  cdleme19d  40566  cdleme19e  40567  cdleme20f  40574  cdleme20k  40579  cdleme20l1  40580  cdleme20l2  40581  cdleme20l  40582  cdleme20m  40583  cdleme21a  40585  cdleme21b  40586  cdleme21c  40587  cdleme21ct  40589  cdleme21d  40590  cdleme21e  40591  cdleme21f  40592  cdleme21i  40595  cdleme22cN  40602  cdleme22eALTN  40605  cdleme25a  40613  cdleme25c  40615  cdleme25dN  40616  cdleme26e  40619  cdleme26ee  40620  cdleme26eALTN  40621  cdleme26f2ALTN  40624  cdleme26f2  40625  cdleme28a  40630  cdleme28b  40631  cdleme28  40633  cdlemefr32sn2aw  40664  cdlemefs32sn1aw  40674  cdleme43fsv1snlem  40680  cdleme41sn3a  40693  cdleme32c  40703  cdleme32e  40705  cdleme32le  40707  cdleme35a  40708  cdleme35b  40710  cdleme35d  40712  cdleme36a  40720  cdleme36m  40721  cdleme39a  40725  cdleme40m  40727  cdleme40n  40728  cdleme43bN  40750  cdleme43dN  40752  cdleme46f2g2  40753  cdleme46f2g1  40754  cdleme4gfv  40767  cdlemeg49le  40771  cdlemeg46c  40773  cdlemeg46fvaw  40776  cdlemeg46nlpq  40777  cdlemeg46gfre  40792  cdleme50trn2  40811  cdlemg2ce  40852  cdlemg2idN  40856  cdlemg7fvbwN  40867  cdlemg10bALTN  40896  cdlemg10a  40900  cdlemg12d  40906  cdlemg12g  40909  cdlemg12  40910  cdlemg13a  40911  cdlemg13  40912  cdlemg17b  40922  cdlemg17dN  40923  cdlemg17dALTN  40924  cdlemg17e  40925  cdlemg17pq  40932  cdlemg17bq  40933  cdlemg18d  40941  cdlemg19a  40943  cdlemg19  40944  cdlemg21  40946  cdlemg27a  40952  cdlemg31b0N  40954  cdlemg27b  40956  cdlemg31c  40959  cdlemg33b0  40961  cdlemg33c0  40962  cdlemg28b  40963  cdlemg33a  40966  cdlemg33  40971  ltrnco  40979  cdlemg44  40993  cdlemg47  40996  tendococl  41032  tendoplcl  41041  cdlemh1  41075  cdlemh2  41076  cdlemh  41077  cdlemi  41080  cdlemk5  41096  cdlemk6  41097  cdlemksel  41105  cdlemksv2  41107  cdlemk7  41108  cdlemk11  41109  cdlemk12  41110  cdlemkole  41113  cdlemk14  41114  cdlemk15  41115  cdlemk16a  41116  cdlemk16  41117  cdlemk1u  41119  cdlemk5u  41121  cdlemk6u  41122  cdlemkuel  41125  cdlemkuv2  41127  cdlemk18  41128  cdlemk19  41129  cdlemk7u  41130  cdlemk11u  41131  cdlemk12u  41132  cdlemk21N  41133  cdlemk20  41134  cdlemkoatnle-2N  41135  cdlemk13-2N  41136  cdlemkole-2N  41137  cdlemk14-2N  41138  cdlemk15-2N  41139  cdlemk16-2N  41140  cdlemk17-2N  41141  cdlemk18-2N  41146  cdlemk19-2N  41147  cdlemk7u-2N  41148  cdlemk11u-2N  41149  cdlemk12u-2N  41150  cdlemk21-2N  41151  cdlemk20-2N  41152  cdlemkuel-3  41158  cdlemkuv2-3N  41159  cdlemk22-3  41161  cdlemk33N  41169  cdlemk47  41209  cdlemk48  41210  cdlemk49  41211  cdlemk50  41212  cdlemk51  41213  cdlemk52  41214  cdlemk53a  41215  cdlemk55b  41220  cdlemkyyN  41222  cdlemk55u1  41225  cdlemk39u1  41227  cdlemk56  41231  dihord1  41478  dihord2a  41479  dihord10  41483  dihord11c  41484  dihord4  41518  dihord5apre  41522  dihglblem2N  41554  dihglbcpreN  41560  dihmeetlem3N  41565  dihjatc1  41571  dihjatc2N  41572  dihjatc3  41573  mapdpglem24  41964  baerlem3lem2  41970  baerlem5alem2  41971  baerlem5blem2  41972  hdmap14lem11  42138  hdmap14lem12  42139  hdmapglem7  42189  mzpsubst  42990  congmul  43209  congsub  43212  ntrclsiso  44308  ntrclskb  44310  ntrclsk3  44311  limsupre  45885  0ellimcdiv  45893  limclner  45895  sge0xaddlem2  46678  clnbgr3stgrgrlim  48265  gpgedgvtx1  48308  lincdifsn  48670  itschlc0yqe  49006  itscnhlc0xyqsol  49011