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 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp113  1323  simp213  1332  simp313  1341  omeu  8572  ackbij1lem16  10229  dvdsgcd  16619  coprimeprodsq  16885  pythagtriplem4  16896  pythagtriplem13  16904  pythagtriplem14  16905  pythagtriplem16  16907  pythagtrip  16911  lsmpropd  19770  matsc  22636  mdetunilem7  22804  smadiadetglem2  22858  m2cpminvid  22939  pmatcollpw1lem1  22960  mp2pm2mplem2  22993  isfil2  24042  filuni  24071  ufprim  24095  cxple2a  26893  isosctr  27015  nolesgn2o  27864  nogesgn1o  27866  sltstr  28009  cofcut2  28144  onsfi  28578  brbtwn2  29284  colinearalg  29289  ax5seg  29317  axcontlem4  29346  measres  34636  bayesth  34853  ofscom  36512  btwndiff  36532  ifscgr  36549  brofs2  36582  brifs2  36583  fscgr  36585  btwnconn1lem1  36592  btwnconn1lem2  36593  btwnconn1lem3  36594  btwnconn1lem4  36595  btwnconn1lem12  36603  seglecgr12im  36615  seglecgr12  36616  ivthALT  36879  islshpcv  39860  eqlkr  39906  lshpsmreu  39916  lshpkrlem5  39921  atlrelat1  40128  cvlcvr1  40146  cvlcvrp  40147  cvlatcvr1  40148  cvlatcvr2  40149  4noncolr3  40260  4noncolr2  40261  4noncolr1  40262  athgt  40263  3dimlem2  40266  3dimlem3a  40267  3dimlem4a  40270  3dimlem4  40271  3dimlem4OLDN  40272  3dim1  40274  3dim2  40275  hlatexch4  40288  ps-2b  40289  3atlem6  40295  llnnleat  40320  2atm  40334  ps-2c  40335  llnmlplnN  40346  2atmat  40368  2llnjN  40374  lvoli2  40388  4atlem3b  40405  4atlem10  40413  4atlem11a  40414  4atlem11b  40415  4atlem12a  40417  4atlem12b  40418  dalemswapyz  40463  lneq2at  40585  2lnat  40591  cdlema1N  40598  cdlemb  40601  pmodlem1  40653  llnmod2i2  40670  dalawlem1  40678  dalawlem3  40680  dalawlem4  40681  dalawlem6  40683  dalawlem9  40686  dalawlem10  40687  dalawlem11  40688  dalawlem12  40689  dalawlem13  40690  dalawlem15  40692  dalaw  40693  pclfinN  40707  osumcllem5N  40767  osumcllem6N  40768  osumcllem7N  40769  osumcllem9N  40771  osumcllem11N  40773  pl42lem1N  40786  lhp2at0  40839  lhp2atne  40841  lhp2at0ne  40843  4atexlem7  40882  ldilco  40923  ltrneq  40956  cdlemd2  41006  cdleme0ex2N  41031  cdleme7aa  41049  cdleme7c  41052  cdleme7d  41053  cdleme7ga  41055  cdleme11c  41068  cdleme11l  41076  cdleme11  41077  cdleme14  41080  cdleme15a  41081  cdleme15c  41083  cdleme16b  41086  cdleme16c  41087  cdleme16d  41088  cdleme16e  41089  cdleme16f  41090  cdleme0nex  41097  cdleme19b  41111  cdleme19d  41113  cdleme19e  41114  cdleme20f  41121  cdleme20k  41126  cdleme20l1  41127  cdleme20l2  41128  cdleme20l  41129  cdleme20m  41130  cdleme21a  41132  cdleme21b  41133  cdleme21c  41134  cdleme21ct  41136  cdleme21d  41137  cdleme21e  41138  cdleme21f  41139  cdleme21i  41142  cdleme22cN  41149  cdleme22eALTN  41152  cdleme25a  41160  cdleme25c  41162  cdleme25dN  41163  cdleme26e  41166  cdleme26ee  41167  cdleme26eALTN  41168  cdleme26f2ALTN  41171  cdleme26f2  41172  cdleme28a  41177  cdleme28b  41178  cdleme28  41180  cdlemefr32sn2aw  41211  cdlemefs32sn1aw  41221  cdleme43fsv1snlem  41227  cdleme41sn3a  41240  cdleme32c  41250  cdleme32e  41252  cdleme32le  41254  cdleme35a  41255  cdleme35b  41257  cdleme35d  41259  cdleme36a  41267  cdleme36m  41268  cdleme39a  41272  cdleme40m  41274  cdleme40n  41275  cdleme43bN  41297  cdleme43dN  41299  cdleme46f2g2  41300  cdleme46f2g1  41301  cdleme4gfv  41314  cdlemeg49le  41318  cdlemeg46c  41320  cdlemeg46fvaw  41323  cdlemeg46nlpq  41324  cdlemeg46gfre  41339  cdleme50trn2  41358  cdlemg2ce  41399  cdlemg2idN  41403  cdlemg7fvbwN  41414  cdlemg10bALTN  41443  cdlemg10a  41447  cdlemg12d  41453  cdlemg12g  41456  cdlemg12  41457  cdlemg13a  41458  cdlemg13  41459  cdlemg17b  41469  cdlemg17dN  41470  cdlemg17dALTN  41471  cdlemg17e  41472  cdlemg17pq  41479  cdlemg17bq  41480  cdlemg18d  41488  cdlemg19a  41490  cdlemg19  41491  cdlemg21  41493  cdlemg27a  41499  cdlemg31b0N  41501  cdlemg27b  41503  cdlemg31c  41506  cdlemg33b0  41508  cdlemg33c0  41509  cdlemg28b  41510  cdlemg33a  41513  cdlemg33  41518  ltrnco  41526  cdlemg44  41540  cdlemg47  41543  tendococl  41579  tendoplcl  41588  cdlemh1  41622  cdlemh2  41623  cdlemh  41624  cdlemi  41627  cdlemk5  41643  cdlemk6  41644  cdlemksel  41652  cdlemksv2  41654  cdlemk7  41655  cdlemk11  41656  cdlemk12  41657  cdlemkole  41660  cdlemk14  41661  cdlemk15  41662  cdlemk16a  41663  cdlemk16  41664  cdlemk1u  41666  cdlemk5u  41668  cdlemk6u  41669  cdlemkuel  41672  cdlemkuv2  41674  cdlemk18  41675  cdlemk19  41676  cdlemk7u  41677  cdlemk11u  41678  cdlemk12u  41679  cdlemk21N  41680  cdlemk20  41681  cdlemkoatnle-2N  41682  cdlemk13-2N  41683  cdlemkole-2N  41684  cdlemk14-2N  41685  cdlemk15-2N  41686  cdlemk16-2N  41687  cdlemk17-2N  41688  cdlemk18-2N  41693  cdlemk19-2N  41694  cdlemk7u-2N  41695  cdlemk11u-2N  41696  cdlemk12u-2N  41697  cdlemk21-2N  41698  cdlemk20-2N  41699  cdlemkuel-3  41705  cdlemkuv2-3N  41706  cdlemk22-3  41708  cdlemk33N  41716  cdlemk47  41756  cdlemk48  41757  cdlemk49  41758  cdlemk50  41759  cdlemk51  41760  cdlemk52  41761  cdlemk53a  41762  cdlemk55b  41767  cdlemkyyN  41769  cdlemk55u1  41772  cdlemk39u1  41774  cdlemk56  41778  dihord1  42025  dihord2a  42026  dihord10  42030  dihord11c  42031  dihord4  42065  dihord5apre  42069  dihglblem2N  42101  dihglbcpreN  42107  dihmeetlem3N  42112  dihjatc1  42118  dihjatc2N  42119  dihjatc3  42120  mapdpglem24  42511  baerlem3lem2  42517  baerlem5alem2  42518  baerlem5blem2  42519  hdmap14lem11  42685  hdmap14lem12  42686  hdmapglem7  42736  mzpsubst  43512  congmul  43727  congsub  43730  ntrclsiso  44826  ntrclskb  44828  ntrclsk3  44829  limsupre  46388  0ellimcdiv  46396  limclner  46398  sge0xaddlem2  47181  clnbgr3stgrgrlim  48817  gpgedgvtx1  48860  lincdifsn  49237  itschlc0yqe  49573  itscnhlc0xyqsol  49578