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  8526  ackbij1lem16  10163  dvdsgcd  16490  coprimeprodsq  16755  pythagtriplem4  16766  pythagtriplem13  16774  pythagtriplem14  16775  pythagtriplem16  16777  pythagtrip  16781  lsmpropd  19583  matsc  22313  mdetunilem7  22481  smadiadetglem2  22535  m2cpminvid  22616  pmatcollpw1lem1  22637  mp2pm2mplem2  22670  isfil2  23719  filuni  23748  ufprim  23772  cxple2a  26584  isosctr  26707  nolesgn2o  27559  nogesgn1o  27561  sslttr  27695  cofcut2  27806  onsfi  28223  brbtwn2  28808  colinearalg  28813  ax5seg  28841  axcontlem4  28870  measres  34185  bayesth  34403  ofscom  35968  btwndiff  35988  ifscgr  36005  brofs2  36038  brifs2  36039  fscgr  36041  btwnconn1lem1  36048  btwnconn1lem2  36049  btwnconn1lem3  36050  btwnconn1lem4  36051  btwnconn1lem12  36059  seglecgr12im  36071  seglecgr12  36072  ivthALT  36296  islshpcv  39019  eqlkr  39065  lshpsmreu  39075  lshpkrlem5  39080  atlrelat1  39287  cvlcvr1  39305  cvlcvrp  39306  cvlatcvr1  39307  cvlatcvr2  39308  4noncolr3  39420  4noncolr2  39421  4noncolr1  39422  athgt  39423  3dimlem2  39426  3dimlem3a  39427  3dimlem4a  39430  3dimlem4  39431  3dimlem4OLDN  39432  3dim1  39434  3dim2  39435  hlatexch4  39448  ps-2b  39449  3atlem6  39455  llnnleat  39480  2atm  39494  ps-2c  39495  llnmlplnN  39506  2atmat  39528  2llnjN  39534  lvoli2  39548  4atlem3b  39565  4atlem10  39573  4atlem11a  39574  4atlem11b  39575  4atlem12a  39577  4atlem12b  39578  dalemswapyz  39623  lneq2at  39745  2lnat  39751  cdlema1N  39758  cdlemb  39761  pmodlem1  39813  llnmod2i2  39830  dalawlem1  39838  dalawlem3  39840  dalawlem4  39841  dalawlem6  39843  dalawlem9  39846  dalawlem10  39847  dalawlem11  39848  dalawlem12  39849  dalawlem13  39850  dalawlem15  39852  dalaw  39853  pclfinN  39867  osumcllem5N  39927  osumcllem6N  39928  osumcllem7N  39929  osumcllem9N  39931  osumcllem11N  39933  pl42lem1N  39946  lhp2at0  39999  lhp2atne  40001  lhp2at0ne  40003  4atexlem7  40042  ldilco  40083  ltrneq  40116  cdlemd2  40166  cdleme0ex2N  40191  cdleme7aa  40209  cdleme7c  40212  cdleme7d  40213  cdleme7ga  40215  cdleme11c  40228  cdleme11l  40236  cdleme11  40237  cdleme14  40240  cdleme15a  40241  cdleme15c  40243  cdleme16b  40246  cdleme16c  40247  cdleme16d  40248  cdleme16e  40249  cdleme16f  40250  cdleme0nex  40257  cdleme19b  40271  cdleme19d  40273  cdleme19e  40274  cdleme20f  40281  cdleme20k  40286  cdleme20l1  40287  cdleme20l2  40288  cdleme20l  40289  cdleme20m  40290  cdleme21a  40292  cdleme21b  40293  cdleme21c  40294  cdleme21ct  40296  cdleme21d  40297  cdleme21e  40298  cdleme21f  40299  cdleme21i  40302  cdleme22cN  40309  cdleme22eALTN  40312  cdleme25a  40320  cdleme25c  40322  cdleme25dN  40323  cdleme26e  40326  cdleme26ee  40327  cdleme26eALTN  40328  cdleme26f2ALTN  40331  cdleme26f2  40332  cdleme28a  40337  cdleme28b  40338  cdleme28  40340  cdlemefr32sn2aw  40371  cdlemefs32sn1aw  40381  cdleme43fsv1snlem  40387  cdleme41sn3a  40400  cdleme32c  40410  cdleme32e  40412  cdleme32le  40414  cdleme35a  40415  cdleme35b  40417  cdleme35d  40419  cdleme36a  40427  cdleme36m  40428  cdleme39a  40432  cdleme40m  40434  cdleme40n  40435  cdleme43bN  40457  cdleme43dN  40459  cdleme46f2g2  40460  cdleme46f2g1  40461  cdleme4gfv  40474  cdlemeg49le  40478  cdlemeg46c  40480  cdlemeg46fvaw  40483  cdlemeg46nlpq  40484  cdlemeg46gfre  40499  cdleme50trn2  40518  cdlemg2ce  40559  cdlemg2idN  40563  cdlemg7fvbwN  40574  cdlemg10bALTN  40603  cdlemg10a  40607  cdlemg12d  40613  cdlemg12g  40616  cdlemg12  40617  cdlemg13a  40618  cdlemg13  40619  cdlemg17b  40629  cdlemg17dN  40630  cdlemg17dALTN  40631  cdlemg17e  40632  cdlemg17pq  40639  cdlemg17bq  40640  cdlemg18d  40648  cdlemg19a  40650  cdlemg19  40651  cdlemg21  40653  cdlemg27a  40659  cdlemg31b0N  40661  cdlemg27b  40663  cdlemg31c  40666  cdlemg33b0  40668  cdlemg33c0  40669  cdlemg28b  40670  cdlemg33a  40673  cdlemg33  40678  ltrnco  40686  cdlemg44  40700  cdlemg47  40703  tendococl  40739  tendoplcl  40748  cdlemh1  40782  cdlemh2  40783  cdlemh  40784  cdlemi  40787  cdlemk5  40803  cdlemk6  40804  cdlemksel  40812  cdlemksv2  40814  cdlemk7  40815  cdlemk11  40816  cdlemk12  40817  cdlemkole  40820  cdlemk14  40821  cdlemk15  40822  cdlemk16a  40823  cdlemk16  40824  cdlemk1u  40826  cdlemk5u  40828  cdlemk6u  40829  cdlemkuel  40832  cdlemkuv2  40834  cdlemk18  40835  cdlemk19  40836  cdlemk7u  40837  cdlemk11u  40838  cdlemk12u  40839  cdlemk21N  40840  cdlemk20  40841  cdlemkoatnle-2N  40842  cdlemk13-2N  40843  cdlemkole-2N  40844  cdlemk14-2N  40845  cdlemk15-2N  40846  cdlemk16-2N  40847  cdlemk17-2N  40848  cdlemk18-2N  40853  cdlemk19-2N  40854  cdlemk7u-2N  40855  cdlemk11u-2N  40856  cdlemk12u-2N  40857  cdlemk21-2N  40858  cdlemk20-2N  40859  cdlemkuel-3  40865  cdlemkuv2-3N  40866  cdlemk22-3  40868  cdlemk33N  40876  cdlemk47  40916  cdlemk48  40917  cdlemk49  40918  cdlemk50  40919  cdlemk51  40920  cdlemk52  40921  cdlemk53a  40922  cdlemk55b  40927  cdlemkyyN  40929  cdlemk55u1  40932  cdlemk39u1  40934  cdlemk56  40938  dihord1  41185  dihord2a  41186  dihord10  41190  dihord11c  41191  dihord4  41225  dihord5apre  41229  dihglblem2N  41261  dihglbcpreN  41267  dihmeetlem3N  41272  dihjatc1  41278  dihjatc2N  41279  dihjatc3  41280  mapdpglem24  41671  baerlem3lem2  41677  baerlem5alem2  41678  baerlem5blem2  41679  hdmap14lem11  41845  hdmap14lem12  41846  hdmapglem7  41896  mzpsubst  42709  congmul  42929  congsub  42932  ntrclsiso  44029  ntrclskb  44031  ntrclsk3  44032  limsupre  45612  0ellimcdiv  45620  limclner  45622  sge0xaddlem2  46405  gpgedgvtx1  48026  lincdifsn  48386  itschlc0yqe  48722  itscnhlc0xyqsol  48727