Theorem simp13 1218

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simp113  1317  simp213  1326  simp313  1335  omeu  8548  ackbij1lem16  10184  dvdsgcd  16569  coprimeprodsq  16835  pythagtriplem4  16846  pythagtriplem13  16854  pythagtriplem14  16855  pythagtriplem16  16857  pythagtrip  16861  lsmpropd  19708  matsc  22498  mdetunilem7  22666  smadiadetglem2  22720  m2cpminvid  22801  pmatcollpw1lem1  22822  mp2pm2mplem2  22855  isfil2  23904  filuni  23933  ufprim  23957  cxple2a  26752  isosctr  26874  nolesgn2o  27723  nogesgn1o  27725  sltstr  27868  cofcut2  28003  onsfi  28437  brbtwn2  29063  colinearalg  29068  ax5seg  29096  axcontlem4  29125  measres  34480  bayesth  34697  ofscom  36318  btwndiff  36338  ifscgr  36355  brofs2  36388  brifs2  36389  fscgr  36391  btwnconn1lem1  36398  btwnconn1lem2  36399  btwnconn1lem3  36400  btwnconn1lem4  36401  btwnconn1lem12  36409  seglecgr12im  36421  seglecgr12  36422  ivthALT  36656  islshpcv  39638  eqlkr  39684  lshpsmreu  39694  lshpkrlem5  39699  atlrelat1  39906  cvlcvr1  39924  cvlcvrp  39925  cvlatcvr1  39926  cvlatcvr2  39927  4noncolr3  40038  4noncolr2  40039  4noncolr1  40040  athgt  40041  3dimlem2  40044  3dimlem3a  40045  3dimlem4a  40048  3dimlem4  40049  3dimlem4OLDN  40050  3dim1  40052  3dim2  40053  hlatexch4  40066  ps-2b  40067  3atlem6  40073  llnnleat  40098  2atm  40112  ps-2c  40113  llnmlplnN  40124  2atmat  40146  2llnjN  40152  lvoli2  40166  4atlem3b  40183  4atlem10  40191  4atlem11a  40192  4atlem11b  40193  4atlem12a  40195  4atlem12b  40196  dalemswapyz  40241  lneq2at  40363  2lnat  40369  cdlema1N  40376  cdlemb  40379  pmodlem1  40431  llnmod2i2  40448  dalawlem1  40456  dalawlem3  40458  dalawlem4  40459  dalawlem6  40461  dalawlem9  40464  dalawlem10  40465  dalawlem11  40466  dalawlem12  40467  dalawlem13  40468  dalawlem15  40470  dalaw  40471  pclfinN  40485  osumcllem5N  40545  osumcllem6N  40546  osumcllem7N  40547  osumcllem9N  40549  osumcllem11N  40551  pl42lem1N  40564  lhp2at0  40617  lhp2atne  40619  lhp2at0ne  40621  4atexlem7  40660  ldilco  40701  ltrneq  40734  cdlemd2  40784  cdleme0ex2N  40809  cdleme7aa  40827  cdleme7c  40830  cdleme7d  40831  cdleme7ga  40833  cdleme11c  40846  cdleme11l  40854  cdleme11  40855  cdleme14  40858  cdleme15a  40859  cdleme15c  40861  cdleme16b  40864  cdleme16c  40865  cdleme16d  40866  cdleme16e  40867  cdleme16f  40868  cdleme0nex  40875  cdleme19b  40889  cdleme19d  40891  cdleme19e  40892  cdleme20f  40899  cdleme20k  40904  cdleme20l1  40905  cdleme20l2  40906  cdleme20l  40907  cdleme20m  40908  cdleme21a  40910  cdleme21b  40911  cdleme21c  40912  cdleme21ct  40914  cdleme21d  40915  cdleme21e  40916  cdleme21f  40917  cdleme21i  40920  cdleme22cN  40927  cdleme22eALTN  40930  cdleme25a  40938  cdleme25c  40940  cdleme25dN  40941  cdleme26e  40944  cdleme26ee  40945  cdleme26eALTN  40946  cdleme26f2ALTN  40949  cdleme26f2  40950  cdleme28a  40955  cdleme28b  40956  cdleme28  40958  cdlemefr32sn2aw  40989  cdlemefs32sn1aw  40999  cdleme43fsv1snlem  41005  cdleme41sn3a  41018  cdleme32c  41028  cdleme32e  41030  cdleme32le  41032  cdleme35a  41033  cdleme35b  41035  cdleme35d  41037  cdleme36a  41045  cdleme36m  41046  cdleme39a  41050  cdleme40m  41052  cdleme40n  41053  cdleme43bN  41075  cdleme43dN  41077  cdleme46f2g2  41078  cdleme46f2g1  41079  cdleme4gfv  41092  cdlemeg49le  41096  cdlemeg46c  41098  cdlemeg46fvaw  41101  cdlemeg46nlpq  41102  cdlemeg46gfre  41117  cdleme50trn2  41136  cdlemg2ce  41177  cdlemg2idN  41181  cdlemg7fvbwN  41192  cdlemg10bALTN  41221  cdlemg10a  41225  cdlemg12d  41231  cdlemg12g  41234  cdlemg12  41235  cdlemg13a  41236  cdlemg13  41237  cdlemg17b  41247  cdlemg17dN  41248  cdlemg17dALTN  41249  cdlemg17e  41250  cdlemg17pq  41257  cdlemg17bq  41258  cdlemg18d  41266  cdlemg19a  41268  cdlemg19  41269  cdlemg21  41271  cdlemg27a  41277  cdlemg31b0N  41279  cdlemg27b  41281  cdlemg31c  41284  cdlemg33b0  41286  cdlemg33c0  41287  cdlemg28b  41288  cdlemg33a  41291  cdlemg33  41296  ltrnco  41304  cdlemg44  41318  cdlemg47  41321  tendococl  41357  tendoplcl  41366  cdlemh1  41400  cdlemh2  41401  cdlemh  41402  cdlemi  41405  cdlemk5  41421  cdlemk6  41422  cdlemksel  41430  cdlemksv2  41432  cdlemk7  41433  cdlemk11  41434  cdlemk12  41435  cdlemkole  41438  cdlemk14  41439  cdlemk15  41440  cdlemk16a  41441  cdlemk16  41442  cdlemk1u  41444  cdlemk5u  41446  cdlemk6u  41447  cdlemkuel  41450  cdlemkuv2  41452  cdlemk18  41453  cdlemk19  41454  cdlemk7u  41455  cdlemk11u  41456  cdlemk12u  41457  cdlemk21N  41458  cdlemk20  41459  cdlemkoatnle-2N  41460  cdlemk13-2N  41461  cdlemkole-2N  41462  cdlemk14-2N  41463  cdlemk15-2N  41464  cdlemk16-2N  41465  cdlemk17-2N  41466  cdlemk18-2N  41471  cdlemk19-2N  41472  cdlemk7u-2N  41473  cdlemk11u-2N  41474  cdlemk12u-2N  41475  cdlemk21-2N  41476  cdlemk20-2N  41477  cdlemkuel-3  41483  cdlemkuv2-3N  41484  cdlemk22-3  41486  cdlemk33N  41494  cdlemk47  41534  cdlemk48  41535  cdlemk49  41536  cdlemk50  41537  cdlemk51  41538  cdlemk52  41539  cdlemk53a  41540  cdlemk55b  41545  cdlemkyyN  41547  cdlemk55u1  41550  cdlemk39u1  41552  cdlemk56  41556  dihord1  41803  dihord2a  41804  dihord10  41808  dihord11c  41809  dihord4  41843  dihord5apre  41847  dihglblem2N  41879  dihglbcpreN  41885  dihmeetlem3N  41890  dihjatc1  41896  dihjatc2N  41897  dihjatc3  41898  mapdpglem24  42289  baerlem3lem2  42295  baerlem5alem2  42296  baerlem5blem2  42297  hdmap14lem11  42463  hdmap14lem12  42464  hdmapglem7  42514  mzpsubst  43290  congmul  43505  congsub  43508  ntrclsiso  44604  ntrclskb  44606  ntrclsk3  44607  limsupre  46176  0ellimcdiv  46184  limclner  46186  sge0xaddlem2  46969  clnbgr3stgrgrlim  48602  gpgedgvtx1  48645  lincdifsn  49007  itschlc0yqe  49343  itscnhlc0xyqsol  49348