Theorem simp13 1224

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  simp113  1323  simp213  1332  simp313  1341  omeu  8571  ackbij1lem16  10218  dvdsgcd  16603  coprimeprodsq  16869  pythagtriplem4  16880  pythagtriplem13  16888  pythagtriplem14  16889  pythagtriplem16  16891  pythagtrip  16895  lsmpropd  19748  matsc  22588  mdetunilem7  22756  smadiadetglem2  22810  m2cpminvid  22891  pmatcollpw1lem1  22912  mp2pm2mplem2  22945  isfil2  23994  filuni  24023  ufprim  24047  cxple2a  26845  isosctr  26967  nolesgn2o  27816  nogesgn1o  27818  sltstr  27961  cofcut2  28096  onsfi  28530  brbtwn2  29236  colinearalg  29241  ax5seg  29269  axcontlem4  29298  measres  34593  bayesth  34810  ofscom  36480  btwndiff  36500  ifscgr  36517  brofs2  36550  brifs2  36551  fscgr  36553  btwnconn1lem1  36560  btwnconn1lem2  36561  btwnconn1lem3  36562  btwnconn1lem4  36563  btwnconn1lem12  36571  seglecgr12im  36583  seglecgr12  36584  ivthALT  36827  islshpcv  39808  eqlkr  39854  lshpsmreu  39864  lshpkrlem5  39869  atlrelat1  40076  cvlcvr1  40094  cvlcvrp  40095  cvlatcvr1  40096  cvlatcvr2  40097  4noncolr3  40208  4noncolr2  40209  4noncolr1  40210  athgt  40211  3dimlem2  40214  3dimlem3a  40215  3dimlem4a  40218  3dimlem4  40219  3dimlem4OLDN  40220  3dim1  40222  3dim2  40223  hlatexch4  40236  ps-2b  40237  3atlem6  40243  llnnleat  40268  2atm  40282  ps-2c  40283  llnmlplnN  40294  2atmat  40316  2llnjN  40322  lvoli2  40336  4atlem3b  40353  4atlem10  40361  4atlem11a  40362  4atlem11b  40363  4atlem12a  40365  4atlem12b  40366  dalemswapyz  40411  lneq2at  40533  2lnat  40539  cdlema1N  40546  cdlemb  40549  pmodlem1  40601  llnmod2i2  40618  dalawlem1  40626  dalawlem3  40628  dalawlem4  40629  dalawlem6  40631  dalawlem9  40634  dalawlem10  40635  dalawlem11  40636  dalawlem12  40637  dalawlem13  40638  dalawlem15  40640  dalaw  40641  pclfinN  40655  osumcllem5N  40715  osumcllem6N  40716  osumcllem7N  40717  osumcllem9N  40719  osumcllem11N  40721  pl42lem1N  40734  lhp2at0  40787  lhp2atne  40789  lhp2at0ne  40791  4atexlem7  40830  ldilco  40871  ltrneq  40904  cdlemd2  40954  cdleme0ex2N  40979  cdleme7aa  40997  cdleme7c  41000  cdleme7d  41001  cdleme7ga  41003  cdleme11c  41016  cdleme11l  41024  cdleme11  41025  cdleme14  41028  cdleme15a  41029  cdleme15c  41031  cdleme16b  41034  cdleme16c  41035  cdleme16d  41036  cdleme16e  41037  cdleme16f  41038  cdleme0nex  41045  cdleme19b  41059  cdleme19d  41061  cdleme19e  41062  cdleme20f  41069  cdleme20k  41074  cdleme20l1  41075  cdleme20l2  41076  cdleme20l  41077  cdleme20m  41078  cdleme21a  41080  cdleme21b  41081  cdleme21c  41082  cdleme21ct  41084  cdleme21d  41085  cdleme21e  41086  cdleme21f  41087  cdleme21i  41090  cdleme22cN  41097  cdleme22eALTN  41100  cdleme25a  41108  cdleme25c  41110  cdleme25dN  41111  cdleme26e  41114  cdleme26ee  41115  cdleme26eALTN  41116  cdleme26f2ALTN  41119  cdleme26f2  41120  cdleme28a  41125  cdleme28b  41126  cdleme28  41128  cdlemefr32sn2aw  41159  cdlemefs32sn1aw  41169  cdleme43fsv1snlem  41175  cdleme41sn3a  41188  cdleme32c  41198  cdleme32e  41200  cdleme32le  41202  cdleme35a  41203  cdleme35b  41205  cdleme35d  41207  cdleme36a  41215  cdleme36m  41216  cdleme39a  41220  cdleme40m  41222  cdleme40n  41223  cdleme43bN  41245  cdleme43dN  41247  cdleme46f2g2  41248  cdleme46f2g1  41249  cdleme4gfv  41262  cdlemeg49le  41266  cdlemeg46c  41268  cdlemeg46fvaw  41271  cdlemeg46nlpq  41272  cdlemeg46gfre  41287  cdleme50trn2  41306  cdlemg2ce  41347  cdlemg2idN  41351  cdlemg7fvbwN  41362  cdlemg10bALTN  41391  cdlemg10a  41395  cdlemg12d  41401  cdlemg12g  41404  cdlemg12  41405  cdlemg13a  41406  cdlemg13  41407  cdlemg17b  41417  cdlemg17dN  41418  cdlemg17dALTN  41419  cdlemg17e  41420  cdlemg17pq  41427  cdlemg17bq  41428  cdlemg18d  41436  cdlemg19a  41438  cdlemg19  41439  cdlemg21  41441  cdlemg27a  41447  cdlemg31b0N  41449  cdlemg27b  41451  cdlemg31c  41454  cdlemg33b0  41456  cdlemg33c0  41457  cdlemg28b  41458  cdlemg33a  41461  cdlemg33  41466  ltrnco  41474  cdlemg44  41488  cdlemg47  41491  tendococl  41527  tendoplcl  41536  cdlemh1  41570  cdlemh2  41571  cdlemh  41572  cdlemi  41575  cdlemk5  41591  cdlemk6  41592  cdlemksel  41600  cdlemksv2  41602  cdlemk7  41603  cdlemk11  41604  cdlemk12  41605  cdlemkole  41608  cdlemk14  41609  cdlemk15  41610  cdlemk16a  41611  cdlemk16  41612  cdlemk1u  41614  cdlemk5u  41616  cdlemk6u  41617  cdlemkuel  41620  cdlemkuv2  41622  cdlemk18  41623  cdlemk19  41624  cdlemk7u  41625  cdlemk11u  41626  cdlemk12u  41627  cdlemk21N  41628  cdlemk20  41629  cdlemkoatnle-2N  41630  cdlemk13-2N  41631  cdlemkole-2N  41632  cdlemk14-2N  41633  cdlemk15-2N  41634  cdlemk16-2N  41635  cdlemk17-2N  41636  cdlemk18-2N  41641  cdlemk19-2N  41642  cdlemk7u-2N  41643  cdlemk11u-2N  41644  cdlemk12u-2N  41645  cdlemk21-2N  41646  cdlemk20-2N  41647  cdlemkuel-3  41653  cdlemkuv2-3N  41654  cdlemk22-3  41656  cdlemk33N  41664  cdlemk47  41704  cdlemk48  41705  cdlemk49  41706  cdlemk50  41707  cdlemk51  41708  cdlemk52  41709  cdlemk53a  41710  cdlemk55b  41715  cdlemkyyN  41717  cdlemk55u1  41720  cdlemk39u1  41722  cdlemk56  41726  dihord1  41973  dihord2a  41974  dihord10  41978  dihord11c  41979  dihord4  42013  dihord5apre  42017  dihglblem2N  42049  dihglbcpreN  42055  dihmeetlem3N  42060  dihjatc1  42066  dihjatc2N  42067  dihjatc3  42068  mapdpglem24  42459  baerlem3lem2  42465  baerlem5alem2  42466  baerlem5blem2  42467  hdmap14lem11  42633  hdmap14lem12  42634  hdmapglem7  42684  mzpsubst  43462  congmul  43677  congsub  43680  ntrclsiso  44776  ntrclskb  44778  ntrclsk3  44779  limsupre  46338  0ellimcdiv  46346  limclner  46348  sge0xaddlem2  47131  clnbgr3stgrgrlim  48767  gpgedgvtx1  48810  lincdifsn  49187  itschlc0yqe  49523  itscnhlc0xyqsol  49528