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  8586  ackbij1lem16  10305  dvdsgcd  16710  coprimeprodsq  16979  pythagtriplem4  16990  pythagtriplem13  16998  pythagtriplem14  16999  pythagtriplem16  17001  pythagtrip  17005  lsmpropd  19884  matsc  22758  mdetunilem7  22926  smadiadetglem2  22980  m2cpminvid  23064  pmatcollpw1lem1  23085  mp2pm2mplem2  23118  isfil2  24168  filuni  24197  ufprim  24221  cxple2a  27020  isosctr  27142  nolesgn2o  28021  nogesgn1o  28023  sltstr  28166  cofcut2  28301  onsfi  28735  brbtwn2  29476  colinearalg  29481  ax5seg  29509  axcontlem4  29538  measres  34848  bayesth  35064  ofscom  36752  btwndiff  36772  ifscgr  36789  brofs2  36822  brifs2  36823  fscgr  36825  btwnconn1lem1  36832  btwnconn1lem2  36833  btwnconn1lem3  36834  btwnconn1lem4  36835  btwnconn1lem12  36843  seglecgr12im  36855  seglecgr12  36856  ivthALT  37103  islshpcv  40090  eqlkr  40136  lshpsmreu  40146  lshpkrlem5  40151  atlrelat1  40358  cvlcvr1  40376  cvlcvrp  40377  cvlatcvr1  40378  cvlatcvr2  40379  4noncolr3  40490  4noncolr2  40491  4noncolr1  40492  athgt  40493  3dimlem2  40496  3dimlem3a  40497  3dimlem4a  40500  3dimlem4  40501  3dimlem4OLDN  40502  3dim1  40504  3dim2  40505  hlatexch4  40518  ps-2b  40519  3atlem6  40525  llnnleat  40550  2atm  40564  ps-2c  40565  llnmlplnN  40576  2atmat  40598  2llnjN  40604  lvoli2  40618  4atlem3b  40635  4atlem10  40643  4atlem11a  40644  4atlem11b  40645  4atlem12a  40647  4atlem12b  40648  dalemswapyz  40693  lneq2at  40815  2lnat  40821  cdlema1N  40828  cdlemb  40831  pmodlem1  40883  llnmod2i2  40900  dalawlem1  40908  dalawlem3  40910  dalawlem4  40911  dalawlem6  40913  dalawlem9  40916  dalawlem10  40917  dalawlem11  40918  dalawlem12  40919  dalawlem13  40920  dalawlem15  40922  dalaw  40923  pclfinN  40937  osumcllem5N  40997  osumcllem6N  40998  osumcllem7N  40999  osumcllem9N  41001  osumcllem11N  41003  pl42lem1N  41016  lhp2at0  41069  lhp2atne  41071  lhp2at0ne  41073  4atexlem7  41112  ldilco  41153  ltrneq  41186  cdlemd2  41236  cdleme0ex2N  41261  cdleme7aa  41279  cdleme7c  41282  cdleme7d  41283  cdleme7ga  41285  cdleme11c  41298  cdleme11l  41306  cdleme11  41307  cdleme14  41310  cdleme15a  41311  cdleme15c  41313  cdleme16b  41316  cdleme16c  41317  cdleme16d  41318  cdleme16e  41319  cdleme16f  41320  cdleme0nex  41327  cdleme19b  41341  cdleme19d  41343  cdleme19e  41344  cdleme20f  41351  cdleme20k  41356  cdleme20l1  41357  cdleme20l2  41358  cdleme20l  41359  cdleme20m  41360  cdleme21a  41362  cdleme21b  41363  cdleme21c  41364  cdleme21ct  41366  cdleme21d  41367  cdleme21e  41368  cdleme21f  41369  cdleme21i  41372  cdleme22cN  41379  cdleme22eALTN  41382  cdleme25a  41390  cdleme25c  41392  cdleme25dN  41393  cdleme26e  41396  cdleme26ee  41397  cdleme26eALTN  41398  cdleme26f2ALTN  41401  cdleme26f2  41402  cdleme28a  41407  cdleme28b  41408  cdleme28  41410  cdlemefr32sn2aw  41441  cdlemefs32sn1aw  41451  cdleme43fsv1snlem  41457  cdleme41sn3a  41470  cdleme32c  41480  cdleme32e  41482  cdleme32le  41484  cdleme35a  41485  cdleme35b  41487  cdleme35d  41489  cdleme36a  41497  cdleme36m  41498  cdleme39a  41502  cdleme40m  41504  cdleme40n  41505  cdleme43bN  41527  cdleme43dN  41529  cdleme46f2g2  41530  cdleme46f2g1  41531  cdleme4gfv  41544  cdlemeg49le  41548  cdlemeg46c  41550  cdlemeg46fvaw  41553  cdlemeg46nlpq  41554  cdlemeg46gfre  41569  cdleme50trn2  41588  cdlemg2ce  41629  cdlemg2idN  41633  cdlemg7fvbwN  41644  cdlemg10bALTN  41673  cdlemg10a  41677  cdlemg12d  41683  cdlemg12g  41686  cdlemg12  41687  cdlemg13a  41688  cdlemg13  41689  cdlemg17b  41699  cdlemg17dN  41700  cdlemg17dALTN  41701  cdlemg17e  41702  cdlemg17pq  41709  cdlemg17bq  41710  cdlemg18d  41718  cdlemg19a  41720  cdlemg19  41721  cdlemg21  41723  cdlemg27a  41729  cdlemg31b0N  41731  cdlemg27b  41733  cdlemg31c  41736  cdlemg33b0  41738  cdlemg33c0  41739  cdlemg28b  41740  cdlemg33a  41743  cdlemg33  41748  ltrnco  41756  cdlemg44  41770  cdlemg47  41773  tendococl  41809  tendoplcl  41818  cdlemh1  41852  cdlemh2  41853  cdlemh  41854  cdlemi  41857  cdlemk5  41873  cdlemk6  41874  cdlemksel  41882  cdlemksv2  41884  cdlemk7  41885  cdlemk11  41886  cdlemk12  41887  cdlemkole  41890  cdlemk14  41891  cdlemk15  41892  cdlemk16a  41893  cdlemk16  41894  cdlemk1u  41896  cdlemk5u  41898  cdlemk6u  41899  cdlemkuel  41902  cdlemkuv2  41904  cdlemk18  41905  cdlemk19  41906  cdlemk7u  41907  cdlemk11u  41908  cdlemk12u  41909  cdlemk21N  41910  cdlemk20  41911  cdlemkoatnle-2N  41912  cdlemk13-2N  41913  cdlemkole-2N  41914  cdlemk14-2N  41915  cdlemk15-2N  41916  cdlemk16-2N  41917  cdlemk17-2N  41918  cdlemk18-2N  41923  cdlemk19-2N  41924  cdlemk7u-2N  41925  cdlemk11u-2N  41926  cdlemk12u-2N  41927  cdlemk21-2N  41928  cdlemk20-2N  41929  cdlemkuel-3  41935  cdlemkuv2-3N  41936  cdlemk22-3  41938  cdlemk33N  41946  cdlemk47  41986  cdlemk48  41987  cdlemk49  41988  cdlemk50  41989  cdlemk51  41990  cdlemk52  41991  cdlemk53a  41992  cdlemk55b  41997  cdlemkyyN  41999  cdlemk55u1  42002  cdlemk39u1  42004  cdlemk56  42008  dihord1  42255  dihord2a  42256  dihord10  42260  dihord11c  42261  dihord4  42295  dihord5apre  42299  dihglblem2N  42331  dihglbcpreN  42337  dihmeetlem3N  42342  dihjatc1  42348  dihjatc2N  42349  dihjatc3  42350  mapdpglem24  42741  baerlem3lem2  42747  baerlem5alem2  42748  baerlem5blem2  42749  hdmap14lem11  42915  hdmap14lem12  42916  hdmapglem7  42966  mzpsubst  43738  congmul  43953  congsub  43956  ntrclsiso  45052  ntrclskb  45054  ntrclsk3  45055  limsupre  46620  0ellimcdiv  46628  limclner  46630  sge0xaddlem2  47413  clnbgr3stgrgrlim  49086  gpgedgvtx1  49129  lincdifsn  49505  itschlc0yqe  49841  itscnhlc0xyqsol  49846