Theorem simp13 1222

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 1103

This theorem is referenced by:  simp113  1321  simp213  1330  simp313  1339  omeu  8566  ackbij1lem16  10213  dvdsgcd  16598  coprimeprodsq  16864  pythagtriplem4  16875  pythagtriplem13  16883  pythagtriplem14  16884  pythagtriplem16  16886  pythagtrip  16890  lsmpropd  19743  matsc  22572  mdetunilem7  22740  smadiadetglem2  22794  m2cpminvid  22875  pmatcollpw1lem1  22896  mp2pm2mplem2  22929  isfil2  23978  filuni  24007  ufprim  24031  cxple2a  26826  isosctr  26948  nolesgn2o  27797  nogesgn1o  27799  sltstr  27942  cofcut2  28077  onsfi  28511  brbtwn2  29192  colinearalg  29197  ax5seg  29225  axcontlem4  29254  measres  34553  bayesth  34770  ofscom  36394  btwndiff  36414  ifscgr  36431  brofs2  36464  brifs2  36465  fscgr  36467  btwnconn1lem1  36474  btwnconn1lem2  36475  btwnconn1lem3  36476  btwnconn1lem4  36477  btwnconn1lem12  36485  seglecgr12im  36497  seglecgr12  36498  ivthALT  36731  islshpcv  39712  eqlkr  39758  lshpsmreu  39768  lshpkrlem5  39773  atlrelat1  39980  cvlcvr1  39998  cvlcvrp  39999  cvlatcvr1  40000  cvlatcvr2  40001  4noncolr3  40112  4noncolr2  40113  4noncolr1  40114  athgt  40115  3dimlem2  40118  3dimlem3a  40119  3dimlem4a  40122  3dimlem4  40123  3dimlem4OLDN  40124  3dim1  40126  3dim2  40127  hlatexch4  40140  ps-2b  40141  3atlem6  40147  llnnleat  40172  2atm  40186  ps-2c  40187  llnmlplnN  40198  2atmat  40220  2llnjN  40226  lvoli2  40240  4atlem3b  40257  4atlem10  40265  4atlem11a  40266  4atlem11b  40267  4atlem12a  40269  4atlem12b  40270  dalemswapyz  40315  lneq2at  40437  2lnat  40443  cdlema1N  40450  cdlemb  40453  pmodlem1  40505  llnmod2i2  40522  dalawlem1  40530  dalawlem3  40532  dalawlem4  40533  dalawlem6  40535  dalawlem9  40538  dalawlem10  40539  dalawlem11  40540  dalawlem12  40541  dalawlem13  40542  dalawlem15  40544  dalaw  40545  pclfinN  40559  osumcllem5N  40619  osumcllem6N  40620  osumcllem7N  40621  osumcllem9N  40623  osumcllem11N  40625  pl42lem1N  40638  lhp2at0  40691  lhp2atne  40693  lhp2at0ne  40695  4atexlem7  40734  ldilco  40775  ltrneq  40808  cdlemd2  40858  cdleme0ex2N  40883  cdleme7aa  40901  cdleme7c  40904  cdleme7d  40905  cdleme7ga  40907  cdleme11c  40920  cdleme11l  40928  cdleme11  40929  cdleme14  40932  cdleme15a  40933  cdleme15c  40935  cdleme16b  40938  cdleme16c  40939  cdleme16d  40940  cdleme16e  40941  cdleme16f  40942  cdleme0nex  40949  cdleme19b  40963  cdleme19d  40965  cdleme19e  40966  cdleme20f  40973  cdleme20k  40978  cdleme20l1  40979  cdleme20l2  40980  cdleme20l  40981  cdleme20m  40982  cdleme21a  40984  cdleme21b  40985  cdleme21c  40986  cdleme21ct  40988  cdleme21d  40989  cdleme21e  40990  cdleme21f  40991  cdleme21i  40994  cdleme22cN  41001  cdleme22eALTN  41004  cdleme25a  41012  cdleme25c  41014  cdleme25dN  41015  cdleme26e  41018  cdleme26ee  41019  cdleme26eALTN  41020  cdleme26f2ALTN  41023  cdleme26f2  41024  cdleme28a  41029  cdleme28b  41030  cdleme28  41032  cdlemefr32sn2aw  41063  cdlemefs32sn1aw  41073  cdleme43fsv1snlem  41079  cdleme41sn3a  41092  cdleme32c  41102  cdleme32e  41104  cdleme32le  41106  cdleme35a  41107  cdleme35b  41109  cdleme35d  41111  cdleme36a  41119  cdleme36m  41120  cdleme39a  41124  cdleme40m  41126  cdleme40n  41127  cdleme43bN  41149  cdleme43dN  41151  cdleme46f2g2  41152  cdleme46f2g1  41153  cdleme4gfv  41166  cdlemeg49le  41170  cdlemeg46c  41172  cdlemeg46fvaw  41175  cdlemeg46nlpq  41176  cdlemeg46gfre  41191  cdleme50trn2  41210  cdlemg2ce  41251  cdlemg2idN  41255  cdlemg7fvbwN  41266  cdlemg10bALTN  41295  cdlemg10a  41299  cdlemg12d  41305  cdlemg12g  41308  cdlemg12  41309  cdlemg13a  41310  cdlemg13  41311  cdlemg17b  41321  cdlemg17dN  41322  cdlemg17dALTN  41323  cdlemg17e  41324  cdlemg17pq  41331  cdlemg17bq  41332  cdlemg18d  41340  cdlemg19a  41342  cdlemg19  41343  cdlemg21  41345  cdlemg27a  41351  cdlemg31b0N  41353  cdlemg27b  41355  cdlemg31c  41358  cdlemg33b0  41360  cdlemg33c0  41361  cdlemg28b  41362  cdlemg33a  41365  cdlemg33  41370  ltrnco  41378  cdlemg44  41392  cdlemg47  41395  tendococl  41431  tendoplcl  41440  cdlemh1  41474  cdlemh2  41475  cdlemh  41476  cdlemi  41479  cdlemk5  41495  cdlemk6  41496  cdlemksel  41504  cdlemksv2  41506  cdlemk7  41507  cdlemk11  41508  cdlemk12  41509  cdlemkole  41512  cdlemk14  41513  cdlemk15  41514  cdlemk16a  41515  cdlemk16  41516  cdlemk1u  41518  cdlemk5u  41520  cdlemk6u  41521  cdlemkuel  41524  cdlemkuv2  41526  cdlemk18  41527  cdlemk19  41528  cdlemk7u  41529  cdlemk11u  41530  cdlemk12u  41531  cdlemk21N  41532  cdlemk20  41533  cdlemkoatnle-2N  41534  cdlemk13-2N  41535  cdlemkole-2N  41536  cdlemk14-2N  41537  cdlemk15-2N  41538  cdlemk16-2N  41539  cdlemk17-2N  41540  cdlemk18-2N  41545  cdlemk19-2N  41546  cdlemk7u-2N  41547  cdlemk11u-2N  41548  cdlemk12u-2N  41549  cdlemk21-2N  41550  cdlemk20-2N  41551  cdlemkuel-3  41557  cdlemkuv2-3N  41558  cdlemk22-3  41560  cdlemk33N  41568  cdlemk47  41608  cdlemk48  41609  cdlemk49  41610  cdlemk50  41611  cdlemk51  41612  cdlemk52  41613  cdlemk53a  41614  cdlemk55b  41619  cdlemkyyN  41621  cdlemk55u1  41624  cdlemk39u1  41626  cdlemk56  41630  dihord1  41877  dihord2a  41878  dihord10  41882  dihord11c  41883  dihord4  41917  dihord5apre  41921  dihglblem2N  41953  dihglbcpreN  41959  dihmeetlem3N  41964  dihjatc1  41970  dihjatc2N  41971  dihjatc3  41972  mapdpglem24  42363  baerlem3lem2  42369  baerlem5alem2  42370  baerlem5blem2  42371  hdmap14lem11  42537  hdmap14lem12  42538  hdmapglem7  42588  mzpsubst  43364  congmul  43579  congsub  43582  ntrclsiso  44678  ntrclskb  44680  ntrclsk3  44681  limsupre  46240  0ellimcdiv  46248  limclner  46250  sge0xaddlem2  47033  clnbgr3stgrgrlim  48666  gpgedgvtx1  48709  lincdifsn  49082  itschlc0yqe  49418  itscnhlc0xyqsol  49423