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  8495  ackbij1lem16  10120  dvdsgcd  16450  coprimeprodsq  16715  pythagtriplem4  16726  pythagtriplem13  16734  pythagtriplem14  16735  pythagtriplem16  16737  pythagtrip  16741  lsmpropd  19584  matsc  22360  mdetunilem7  22528  smadiadetglem2  22582  m2cpminvid  22663  pmatcollpw1lem1  22684  mp2pm2mplem2  22717  isfil2  23766  filuni  23795  ufprim  23819  cxple2a  26630  isosctr  26753  nolesgn2o  27605  nogesgn1o  27607  sslttr  27743  cofcut2  27861  onsfi  28278  brbtwn2  28878  colinearalg  28883  ax5seg  28911  axcontlem4  28940  measres  34227  bayesth  34444  ofscom  36041  btwndiff  36061  ifscgr  36078  brofs2  36111  brifs2  36112  fscgr  36114  btwnconn1lem1  36121  btwnconn1lem2  36122  btwnconn1lem3  36123  btwnconn1lem4  36124  btwnconn1lem12  36132  seglecgr12im  36144  seglecgr12  36145  ivthALT  36369  islshpcv  39092  eqlkr  39138  lshpsmreu  39148  lshpkrlem5  39153  atlrelat1  39360  cvlcvr1  39378  cvlcvrp  39379  cvlatcvr1  39380  cvlatcvr2  39381  4noncolr3  39492  4noncolr2  39493  4noncolr1  39494  athgt  39495  3dimlem2  39498  3dimlem3a  39499  3dimlem4a  39502  3dimlem4  39503  3dimlem4OLDN  39504  3dim1  39506  3dim2  39507  hlatexch4  39520  ps-2b  39521  3atlem6  39527  llnnleat  39552  2atm  39566  ps-2c  39567  llnmlplnN  39578  2atmat  39600  2llnjN  39606  lvoli2  39620  4atlem3b  39637  4atlem10  39645  4atlem11a  39646  4atlem11b  39647  4atlem12a  39649  4atlem12b  39650  dalemswapyz  39695  lneq2at  39817  2lnat  39823  cdlema1N  39830  cdlemb  39833  pmodlem1  39885  llnmod2i2  39902  dalawlem1  39910  dalawlem3  39912  dalawlem4  39913  dalawlem6  39915  dalawlem9  39918  dalawlem10  39919  dalawlem11  39920  dalawlem12  39921  dalawlem13  39922  dalawlem15  39924  dalaw  39925  pclfinN  39939  osumcllem5N  39999  osumcllem6N  40000  osumcllem7N  40001  osumcllem9N  40003  osumcllem11N  40005  pl42lem1N  40018  lhp2at0  40071  lhp2atne  40073  lhp2at0ne  40075  4atexlem7  40114  ldilco  40155  ltrneq  40188  cdlemd2  40238  cdleme0ex2N  40263  cdleme7aa  40281  cdleme7c  40284  cdleme7d  40285  cdleme7ga  40287  cdleme11c  40300  cdleme11l  40308  cdleme11  40309  cdleme14  40312  cdleme15a  40313  cdleme15c  40315  cdleme16b  40318  cdleme16c  40319  cdleme16d  40320  cdleme16e  40321  cdleme16f  40322  cdleme0nex  40329  cdleme19b  40343  cdleme19d  40345  cdleme19e  40346  cdleme20f  40353  cdleme20k  40358  cdleme20l1  40359  cdleme20l2  40360  cdleme20l  40361  cdleme20m  40362  cdleme21a  40364  cdleme21b  40365  cdleme21c  40366  cdleme21ct  40368  cdleme21d  40369  cdleme21e  40370  cdleme21f  40371  cdleme21i  40374  cdleme22cN  40381  cdleme22eALTN  40384  cdleme25a  40392  cdleme25c  40394  cdleme25dN  40395  cdleme26e  40398  cdleme26ee  40399  cdleme26eALTN  40400  cdleme26f2ALTN  40403  cdleme26f2  40404  cdleme28a  40409  cdleme28b  40410  cdleme28  40412  cdlemefr32sn2aw  40443  cdlemefs32sn1aw  40453  cdleme43fsv1snlem  40459  cdleme41sn3a  40472  cdleme32c  40482  cdleme32e  40484  cdleme32le  40486  cdleme35a  40487  cdleme35b  40489  cdleme35d  40491  cdleme36a  40499  cdleme36m  40500  cdleme39a  40504  cdleme40m  40506  cdleme40n  40507  cdleme43bN  40529  cdleme43dN  40531  cdleme46f2g2  40532  cdleme46f2g1  40533  cdleme4gfv  40546  cdlemeg49le  40550  cdlemeg46c  40552  cdlemeg46fvaw  40555  cdlemeg46nlpq  40556  cdlemeg46gfre  40571  cdleme50trn2  40590  cdlemg2ce  40631  cdlemg2idN  40635  cdlemg7fvbwN  40646  cdlemg10bALTN  40675  cdlemg10a  40679  cdlemg12d  40685  cdlemg12g  40688  cdlemg12  40689  cdlemg13a  40690  cdlemg13  40691  cdlemg17b  40701  cdlemg17dN  40702  cdlemg17dALTN  40703  cdlemg17e  40704  cdlemg17pq  40711  cdlemg17bq  40712  cdlemg18d  40720  cdlemg19a  40722  cdlemg19  40723  cdlemg21  40725  cdlemg27a  40731  cdlemg31b0N  40733  cdlemg27b  40735  cdlemg31c  40738  cdlemg33b0  40740  cdlemg33c0  40741  cdlemg28b  40742  cdlemg33a  40745  cdlemg33  40750  ltrnco  40758  cdlemg44  40772  cdlemg47  40775  tendococl  40811  tendoplcl  40820  cdlemh1  40854  cdlemh2  40855  cdlemh  40856  cdlemi  40859  cdlemk5  40875  cdlemk6  40876  cdlemksel  40884  cdlemksv2  40886  cdlemk7  40887  cdlemk11  40888  cdlemk12  40889  cdlemkole  40892  cdlemk14  40893  cdlemk15  40894  cdlemk16a  40895  cdlemk16  40896  cdlemk1u  40898  cdlemk5u  40900  cdlemk6u  40901  cdlemkuel  40904  cdlemkuv2  40906  cdlemk18  40907  cdlemk19  40908  cdlemk7u  40909  cdlemk11u  40910  cdlemk12u  40911  cdlemk21N  40912  cdlemk20  40913  cdlemkoatnle-2N  40914  cdlemk13-2N  40915  cdlemkole-2N  40916  cdlemk14-2N  40917  cdlemk15-2N  40918  cdlemk16-2N  40919  cdlemk17-2N  40920  cdlemk18-2N  40925  cdlemk19-2N  40926  cdlemk7u-2N  40927  cdlemk11u-2N  40928  cdlemk12u-2N  40929  cdlemk21-2N  40930  cdlemk20-2N  40931  cdlemkuel-3  40937  cdlemkuv2-3N  40938  cdlemk22-3  40940  cdlemk33N  40948  cdlemk47  40988  cdlemk48  40989  cdlemk49  40990  cdlemk50  40991  cdlemk51  40992  cdlemk52  40993  cdlemk53a  40994  cdlemk55b  40999  cdlemkyyN  41001  cdlemk55u1  41004  cdlemk39u1  41006  cdlemk56  41010  dihord1  41257  dihord2a  41258  dihord10  41262  dihord11c  41263  dihord4  41297  dihord5apre  41301  dihglblem2N  41333  dihglbcpreN  41339  dihmeetlem3N  41344  dihjatc1  41350  dihjatc2N  41351  dihjatc3  41352  mapdpglem24  41743  baerlem3lem2  41749  baerlem5alem2  41750  baerlem5blem2  41751  hdmap14lem11  41917  hdmap14lem12  41918  hdmapglem7  41968  mzpsubst  42781  congmul  43000  congsub  43003  ntrclsiso  44100  ntrclskb  44102  ntrclsk3  44103  limsupre  45679  0ellimcdiv  45687  limclner  45689  sge0xaddlem2  46472  clnbgr3stgrgrlim  48050  gpgedgvtx1  48093  lincdifsn  48456  itschlc0yqe  48792  itscnhlc0xyqsol  48797