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  8509  ackbij1lem16  10136  dvdsgcd  16462  coprimeprodsq  16727  pythagtriplem4  16738  pythagtriplem13  16746  pythagtriplem14  16747  pythagtriplem16  16749  pythagtrip  16753  lsmpropd  19597  matsc  22385  mdetunilem7  22553  smadiadetglem2  22607  m2cpminvid  22688  pmatcollpw1lem1  22709  mp2pm2mplem2  22742  isfil2  23791  filuni  23820  ufprim  23844  cxple2a  26655  isosctr  26778  nolesgn2o  27630  nogesgn1o  27632  sslttr  27768  cofcut2  27886  onsfi  28303  brbtwn2  28904  colinearalg  28909  ax5seg  28937  axcontlem4  28966  measres  34307  bayesth  34524  ofscom  36123  btwndiff  36143  ifscgr  36160  brofs2  36193  brifs2  36194  fscgr  36196  btwnconn1lem1  36203  btwnconn1lem2  36204  btwnconn1lem3  36205  btwnconn1lem4  36206  btwnconn1lem12  36214  seglecgr12im  36226  seglecgr12  36227  ivthALT  36451  islshpcv  39225  eqlkr  39271  lshpsmreu  39281  lshpkrlem5  39286  atlrelat1  39493  cvlcvr1  39511  cvlcvrp  39512  cvlatcvr1  39513  cvlatcvr2  39514  4noncolr3  39625  4noncolr2  39626  4noncolr1  39627  athgt  39628  3dimlem2  39631  3dimlem3a  39632  3dimlem4a  39635  3dimlem4  39636  3dimlem4OLDN  39637  3dim1  39639  3dim2  39640  hlatexch4  39653  ps-2b  39654  3atlem6  39660  llnnleat  39685  2atm  39699  ps-2c  39700  llnmlplnN  39711  2atmat  39733  2llnjN  39739  lvoli2  39753  4atlem3b  39770  4atlem10  39778  4atlem11a  39779  4atlem11b  39780  4atlem12a  39782  4atlem12b  39783  dalemswapyz  39828  lneq2at  39950  2lnat  39956  cdlema1N  39963  cdlemb  39966  pmodlem1  40018  llnmod2i2  40035  dalawlem1  40043  dalawlem3  40045  dalawlem4  40046  dalawlem6  40048  dalawlem9  40051  dalawlem10  40052  dalawlem11  40053  dalawlem12  40054  dalawlem13  40055  dalawlem15  40057  dalaw  40058  pclfinN  40072  osumcllem5N  40132  osumcllem6N  40133  osumcllem7N  40134  osumcllem9N  40136  osumcllem11N  40138  pl42lem1N  40151  lhp2at0  40204  lhp2atne  40206  lhp2at0ne  40208  4atexlem7  40247  ldilco  40288  ltrneq  40321  cdlemd2  40371  cdleme0ex2N  40396  cdleme7aa  40414  cdleme7c  40417  cdleme7d  40418  cdleme7ga  40420  cdleme11c  40433  cdleme11l  40441  cdleme11  40442  cdleme14  40445  cdleme15a  40446  cdleme15c  40448  cdleme16b  40451  cdleme16c  40452  cdleme16d  40453  cdleme16e  40454  cdleme16f  40455  cdleme0nex  40462  cdleme19b  40476  cdleme19d  40478  cdleme19e  40479  cdleme20f  40486  cdleme20k  40491  cdleme20l1  40492  cdleme20l2  40493  cdleme20l  40494  cdleme20m  40495  cdleme21a  40497  cdleme21b  40498  cdleme21c  40499  cdleme21ct  40501  cdleme21d  40502  cdleme21e  40503  cdleme21f  40504  cdleme21i  40507  cdleme22cN  40514  cdleme22eALTN  40517  cdleme25a  40525  cdleme25c  40527  cdleme25dN  40528  cdleme26e  40531  cdleme26ee  40532  cdleme26eALTN  40533  cdleme26f2ALTN  40536  cdleme26f2  40537  cdleme28a  40542  cdleme28b  40543  cdleme28  40545  cdlemefr32sn2aw  40576  cdlemefs32sn1aw  40586  cdleme43fsv1snlem  40592  cdleme41sn3a  40605  cdleme32c  40615  cdleme32e  40617  cdleme32le  40619  cdleme35a  40620  cdleme35b  40622  cdleme35d  40624  cdleme36a  40632  cdleme36m  40633  cdleme39a  40637  cdleme40m  40639  cdleme40n  40640  cdleme43bN  40662  cdleme43dN  40664  cdleme46f2g2  40665  cdleme46f2g1  40666  cdleme4gfv  40679  cdlemeg49le  40683  cdlemeg46c  40685  cdlemeg46fvaw  40688  cdlemeg46nlpq  40689  cdlemeg46gfre  40704  cdleme50trn2  40723  cdlemg2ce  40764  cdlemg2idN  40768  cdlemg7fvbwN  40779  cdlemg10bALTN  40808  cdlemg10a  40812  cdlemg12d  40818  cdlemg12g  40821  cdlemg12  40822  cdlemg13a  40823  cdlemg13  40824  cdlemg17b  40834  cdlemg17dN  40835  cdlemg17dALTN  40836  cdlemg17e  40837  cdlemg17pq  40844  cdlemg17bq  40845  cdlemg18d  40853  cdlemg19a  40855  cdlemg19  40856  cdlemg21  40858  cdlemg27a  40864  cdlemg31b0N  40866  cdlemg27b  40868  cdlemg31c  40871  cdlemg33b0  40873  cdlemg33c0  40874  cdlemg28b  40875  cdlemg33a  40878  cdlemg33  40883  ltrnco  40891  cdlemg44  40905  cdlemg47  40908  tendococl  40944  tendoplcl  40953  cdlemh1  40987  cdlemh2  40988  cdlemh  40989  cdlemi  40992  cdlemk5  41008  cdlemk6  41009  cdlemksel  41017  cdlemksv2  41019  cdlemk7  41020  cdlemk11  41021  cdlemk12  41022  cdlemkole  41025  cdlemk14  41026  cdlemk15  41027  cdlemk16a  41028  cdlemk16  41029  cdlemk1u  41031  cdlemk5u  41033  cdlemk6u  41034  cdlemkuel  41037  cdlemkuv2  41039  cdlemk18  41040  cdlemk19  41041  cdlemk7u  41042  cdlemk11u  41043  cdlemk12u  41044  cdlemk21N  41045  cdlemk20  41046  cdlemkoatnle-2N  41047  cdlemk13-2N  41048  cdlemkole-2N  41049  cdlemk14-2N  41050  cdlemk15-2N  41051  cdlemk16-2N  41052  cdlemk17-2N  41053  cdlemk18-2N  41058  cdlemk19-2N  41059  cdlemk7u-2N  41060  cdlemk11u-2N  41061  cdlemk12u-2N  41062  cdlemk21-2N  41063  cdlemk20-2N  41064  cdlemkuel-3  41070  cdlemkuv2-3N  41071  cdlemk22-3  41073  cdlemk33N  41081  cdlemk47  41121  cdlemk48  41122  cdlemk49  41123  cdlemk50  41124  cdlemk51  41125  cdlemk52  41126  cdlemk53a  41127  cdlemk55b  41132  cdlemkyyN  41134  cdlemk55u1  41137  cdlemk39u1  41139  cdlemk56  41143  dihord1  41390  dihord2a  41391  dihord10  41395  dihord11c  41396  dihord4  41430  dihord5apre  41434  dihglblem2N  41466  dihglbcpreN  41472  dihmeetlem3N  41477  dihjatc1  41483  dihjatc2N  41484  dihjatc3  41485  mapdpglem24  41876  baerlem3lem2  41882  baerlem5alem2  41883  baerlem5blem2  41884  hdmap14lem11  42050  hdmap14lem12  42051  hdmapglem7  42101  mzpsubst  42905  congmul  43124  congsub  43127  ntrclsiso  44224  ntrclskb  44226  ntrclsk3  44227  limsupre  45801  0ellimcdiv  45809  limclner  45811  sge0xaddlem2  46594  clnbgr3stgrgrlim  48181  gpgedgvtx1  48224  lincdifsn  48586  itschlc0yqe  48922  itscnhlc0xyqsol  48927