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

This theorem is used by:  simp113  1323  simp213  1332  simp313  1341  omeu  8566  ackbij1lem16  10222  dvdsgcd  16606  coprimeprodsq  16872  pythagtriplem4  16883  pythagtriplem13  16891  pythagtriplem14  16892  pythagtriplem16  16894  pythagtrip  16898  lsmpropd  19751  matsc  22616  mdetunilem7  22784  smadiadetglem2  22838  m2cpminvid  22919  pmatcollpw1lem1  22940  mp2pm2mplem2  22973  isfil2  24022  filuni  24051  ufprim  24075  cxple2a  26873  isosctr  26995  nolesgn2o  27844  nogesgn1o  27846  sltstr  27989  cofcut2  28124  onsfi  28558  brbtwn2  29264  colinearalg  29269  ax5seg  29297  axcontlem4  29326  measres  34621  bayesth  34838  ofscom  36507  btwndiff  36527  ifscgr  36544  brofs2  36577  brifs2  36578  fscgr  36580  btwnconn1lem1  36587  btwnconn1lem2  36588  btwnconn1lem3  36589  btwnconn1lem4  36590  btwnconn1lem12  36598  seglecgr12im  36610  seglecgr12  36611  ivthALT  36874  islshpcv  39855  eqlkr  39901  lshpsmreu  39911  lshpkrlem5  39916  atlrelat1  40123  cvlcvr1  40141  cvlcvrp  40142  cvlatcvr1  40143  cvlatcvr2  40144  4noncolr3  40255  4noncolr2  40256  4noncolr1  40257  athgt  40258  3dimlem2  40261  3dimlem3a  40262  3dimlem4a  40265  3dimlem4  40266  3dimlem4OLDN  40267  3dim1  40269  3dim2  40270  hlatexch4  40283  ps-2b  40284  3atlem6  40290  llnnleat  40315  2atm  40329  ps-2c  40330  llnmlplnN  40341  2atmat  40363  2llnjN  40369  lvoli2  40383  4atlem3b  40400  4atlem10  40408  4atlem11a  40409  4atlem11b  40410  4atlem12a  40412  4atlem12b  40413  dalemswapyz  40458  lneq2at  40580  2lnat  40586  cdlema1N  40593  cdlemb  40596  pmodlem1  40648  llnmod2i2  40665  dalawlem1  40673  dalawlem3  40675  dalawlem4  40676  dalawlem6  40678  dalawlem9  40681  dalawlem10  40682  dalawlem11  40683  dalawlem12  40684  dalawlem13  40685  dalawlem15  40687  dalaw  40688  pclfinN  40702  osumcllem5N  40762  osumcllem6N  40763  osumcllem7N  40764  osumcllem9N  40766  osumcllem11N  40768  pl42lem1N  40781  lhp2at0  40834  lhp2atne  40836  lhp2at0ne  40838  4atexlem7  40877  ldilco  40918  ltrneq  40951  cdlemd2  41001  cdleme0ex2N  41026  cdleme7aa  41044  cdleme7c  41047  cdleme7d  41048  cdleme7ga  41050  cdleme11c  41063  cdleme11l  41071  cdleme11  41072  cdleme14  41075  cdleme15a  41076  cdleme15c  41078  cdleme16b  41081  cdleme16c  41082  cdleme16d  41083  cdleme16e  41084  cdleme16f  41085  cdleme0nex  41092  cdleme19b  41106  cdleme19d  41108  cdleme19e  41109  cdleme20f  41116  cdleme20k  41121  cdleme20l1  41122  cdleme20l2  41123  cdleme20l  41124  cdleme20m  41125  cdleme21a  41127  cdleme21b  41128  cdleme21c  41129  cdleme21ct  41131  cdleme21d  41132  cdleme21e  41133  cdleme21f  41134  cdleme21i  41137  cdleme22cN  41144  cdleme22eALTN  41147  cdleme25a  41155  cdleme25c  41157  cdleme25dN  41158  cdleme26e  41161  cdleme26ee  41162  cdleme26eALTN  41163  cdleme26f2ALTN  41166  cdleme26f2  41167  cdleme28a  41172  cdleme28b  41173  cdleme28  41175  cdlemefr32sn2aw  41206  cdlemefs32sn1aw  41216  cdleme43fsv1snlem  41222  cdleme41sn3a  41235  cdleme32c  41245  cdleme32e  41247  cdleme32le  41249  cdleme35a  41250  cdleme35b  41252  cdleme35d  41254  cdleme36a  41262  cdleme36m  41263  cdleme39a  41267  cdleme40m  41269  cdleme40n  41270  cdleme43bN  41292  cdleme43dN  41294  cdleme46f2g2  41295  cdleme46f2g1  41296  cdleme4gfv  41309  cdlemeg49le  41313  cdlemeg46c  41315  cdlemeg46fvaw  41318  cdlemeg46nlpq  41319  cdlemeg46gfre  41334  cdleme50trn2  41353  cdlemg2ce  41394  cdlemg2idN  41398  cdlemg7fvbwN  41409  cdlemg10bALTN  41438  cdlemg10a  41442  cdlemg12d  41448  cdlemg12g  41451  cdlemg12  41452  cdlemg13a  41453  cdlemg13  41454  cdlemg17b  41464  cdlemg17dN  41465  cdlemg17dALTN  41466  cdlemg17e  41467  cdlemg17pq  41474  cdlemg17bq  41475  cdlemg18d  41483  cdlemg19a  41485  cdlemg19  41486  cdlemg21  41488  cdlemg27a  41494  cdlemg31b0N  41496  cdlemg27b  41498  cdlemg31c  41501  cdlemg33b0  41503  cdlemg33c0  41504  cdlemg28b  41505  cdlemg33a  41508  cdlemg33  41513  ltrnco  41521  cdlemg44  41535  cdlemg47  41538  tendococl  41574  tendoplcl  41583  cdlemh1  41617  cdlemh2  41618  cdlemh  41619  cdlemi  41622  cdlemk5  41638  cdlemk6  41639  cdlemksel  41647  cdlemksv2  41649  cdlemk7  41650  cdlemk11  41651  cdlemk12  41652  cdlemkole  41655  cdlemk14  41656  cdlemk15  41657  cdlemk16a  41658  cdlemk16  41659  cdlemk1u  41661  cdlemk5u  41663  cdlemk6u  41664  cdlemkuel  41667  cdlemkuv2  41669  cdlemk18  41670  cdlemk19  41671  cdlemk7u  41672  cdlemk11u  41673  cdlemk12u  41674  cdlemk21N  41675  cdlemk20  41676  cdlemkoatnle-2N  41677  cdlemk13-2N  41678  cdlemkole-2N  41679  cdlemk14-2N  41680  cdlemk15-2N  41681  cdlemk16-2N  41682  cdlemk17-2N  41683  cdlemk18-2N  41688  cdlemk19-2N  41689  cdlemk7u-2N  41690  cdlemk11u-2N  41691  cdlemk12u-2N  41692  cdlemk21-2N  41693  cdlemk20-2N  41694  cdlemkuel-3  41700  cdlemkuv2-3N  41701  cdlemk22-3  41703  cdlemk33N  41711  cdlemk47  41751  cdlemk48  41752  cdlemk49  41753  cdlemk50  41754  cdlemk51  41755  cdlemk52  41756  cdlemk53a  41757  cdlemk55b  41762  cdlemkyyN  41764  cdlemk55u1  41767  cdlemk39u1  41769  cdlemk56  41773  dihord1  42020  dihord2a  42021  dihord10  42025  dihord11c  42026  dihord4  42060  dihord5apre  42064  dihglblem2N  42096  dihglbcpreN  42102  dihmeetlem3N  42107  dihjatc1  42113  dihjatc2N  42114  dihjatc3  42115  mapdpglem24  42506  baerlem3lem2  42512  baerlem5alem2  42513  baerlem5blem2  42514  hdmap14lem11  42680  hdmap14lem12  42681  hdmapglem7  42731  mzpsubst  43507  congmul  43722  congsub  43725  ntrclsiso  44821  ntrclskb  44823  ntrclsk3  44824  limsupre  46383  0ellimcdiv  46391  limclner  46393  sge0xaddlem2  47176  clnbgr3stgrgrlim  48812  gpgedgvtx1  48855  lincdifsn  49232  itschlc0yqe  49568  itscnhlc0xyqsol  49573