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  8597  ackbij1lem16  10316  dvdsgcd  16723  coprimeprodsq  16992  pythagtriplem4  17003  pythagtriplem13  17011  pythagtriplem14  17012  pythagtriplem16  17014  pythagtrip  17018  lsmpropd  19897  matsc  22771  mdetunilem7  22939  smadiadetglem2  22993  m2cpminvid  23077  pmatcollpw1lem1  23098  mp2pm2mplem2  23131  isfil2  24181  filuni  24210  ufprim  24234  cxple2a  27033  isosctr  27155  nolesgn2o  28034  nogesgn1o  28036  sltstr  28179  cofcut2  28314  onsfi  28748  brbtwn2  29489  colinearalg  29494  ax5seg  29522  axcontlem4  29551  measres  34902  bayesth  35118  ofscom  36865  btwndiff  36885  ifscgr  36902  brofs2  36935  brifs2  36936  fscgr  36938  btwnconn1lem1  36945  btwnconn1lem2  36946  btwnconn1lem3  36947  btwnconn1lem4  36948  btwnconn1lem12  36956  seglecgr12im  36968  seglecgr12  36969  ivthALT  37216  islshpcv  40204  eqlkr  40250  lshpsmreu  40260  lshpkrlem5  40265  atlrelat1  40472  cvlcvr1  40490  cvlcvrp  40491  cvlatcvr1  40492  cvlatcvr2  40493  4noncolr3  40604  4noncolr2  40605  4noncolr1  40606  athgt  40607  3dimlem2  40610  3dimlem3a  40611  3dimlem4a  40614  3dimlem4  40615  3dimlem4OLDN  40616  3dim1  40618  3dim2  40619  hlatexch4  40632  ps-2b  40633  3atlem6  40639  llnnleat  40664  2atm  40678  ps-2c  40679  llnmlplnN  40690  2atmat  40712  2llnjN  40718  lvoli2  40732  4atlem3b  40749  4atlem10  40757  4atlem11a  40758  4atlem11b  40759  4atlem12a  40761  4atlem12b  40762  dalemswapyz  40807  lneq2at  40929  2lnat  40935  cdlema1N  40942  cdlemb  40945  pmodlem1  40997  llnmod2i2  41014  dalawlem1  41022  dalawlem3  41024  dalawlem4  41025  dalawlem6  41027  dalawlem9  41030  dalawlem10  41031  dalawlem11  41032  dalawlem12  41033  dalawlem13  41034  dalawlem15  41036  dalaw  41037  pclfinN  41051  osumcllem5N  41111  osumcllem6N  41112  osumcllem7N  41113  osumcllem9N  41115  osumcllem11N  41117  pl42lem1N  41130  lhp2at0  41183  lhp2atne  41185  lhp2at0ne  41187  4atexlem7  41226  ldilco  41267  ltrneq  41300  cdlemd2  41350  cdleme0ex2N  41375  cdleme7aa  41393  cdleme7c  41396  cdleme7d  41397  cdleme7ga  41399  cdleme11c  41412  cdleme11l  41420  cdleme11  41421  cdleme14  41424  cdleme15a  41425  cdleme15c  41427  cdleme16b  41430  cdleme16c  41431  cdleme16d  41432  cdleme16e  41433  cdleme16f  41434  cdleme0nex  41441  cdleme19b  41455  cdleme19d  41457  cdleme19e  41458  cdleme20f  41465  cdleme20k  41470  cdleme20l1  41471  cdleme20l2  41472  cdleme20l  41473  cdleme20m  41474  cdleme21a  41476  cdleme21b  41477  cdleme21c  41478  cdleme21ct  41480  cdleme21d  41481  cdleme21e  41482  cdleme21f  41483  cdleme21i  41486  cdleme22cN  41493  cdleme22eALTN  41496  cdleme25a  41504  cdleme25c  41506  cdleme25dN  41507  cdleme26e  41510  cdleme26ee  41511  cdleme26eALTN  41512  cdleme26f2ALTN  41515  cdleme26f2  41516  cdleme28a  41521  cdleme28b  41522  cdleme28  41524  cdlemefr32sn2aw  41555  cdlemefs32sn1aw  41565  cdleme43fsv1snlem  41571  cdleme41sn3a  41584  cdleme32c  41594  cdleme32e  41596  cdleme32le  41598  cdleme35a  41599  cdleme35b  41601  cdleme35d  41603  cdleme36a  41611  cdleme36m  41612  cdleme39a  41616  cdleme40m  41618  cdleme40n  41619  cdleme43bN  41641  cdleme43dN  41643  cdleme46f2g2  41644  cdleme46f2g1  41645  cdleme4gfv  41658  cdlemeg49le  41662  cdlemeg46c  41664  cdlemeg46fvaw  41667  cdlemeg46nlpq  41668  cdlemeg46gfre  41683  cdleme50trn2  41702  cdlemg2ce  41743  cdlemg2idN  41747  cdlemg7fvbwN  41758  cdlemg10bALTN  41787  cdlemg10a  41791  cdlemg12d  41797  cdlemg12g  41800  cdlemg12  41801  cdlemg13a  41802  cdlemg13  41803  cdlemg17b  41813  cdlemg17dN  41814  cdlemg17dALTN  41815  cdlemg17e  41816  cdlemg17pq  41823  cdlemg17bq  41824  cdlemg18d  41832  cdlemg19a  41834  cdlemg19  41835  cdlemg21  41837  cdlemg27a  41843  cdlemg31b0N  41845  cdlemg27b  41847  cdlemg31c  41850  cdlemg33b0  41852  cdlemg33c0  41853  cdlemg28b  41854  cdlemg33a  41857  cdlemg33  41862  ltrnco  41870  cdlemg44  41884  cdlemg47  41887  tendococl  41923  tendoplcl  41932  cdlemh1  41966  cdlemh2  41967  cdlemh  41968  cdlemi  41971  cdlemk5  41987  cdlemk6  41988  cdlemksel  41996  cdlemksv2  41998  cdlemk7  41999  cdlemk11  42000  cdlemk12  42001  cdlemkole  42004  cdlemk14  42005  cdlemk15  42006  cdlemk16a  42007  cdlemk16  42008  cdlemk1u  42010  cdlemk5u  42012  cdlemk6u  42013  cdlemkuel  42016  cdlemkuv2  42018  cdlemk18  42019  cdlemk19  42020  cdlemk7u  42021  cdlemk11u  42022  cdlemk12u  42023  cdlemk21N  42024  cdlemk20  42025  cdlemkoatnle-2N  42026  cdlemk13-2N  42027  cdlemkole-2N  42028  cdlemk14-2N  42029  cdlemk15-2N  42030  cdlemk16-2N  42031  cdlemk17-2N  42032  cdlemk18-2N  42037  cdlemk19-2N  42038  cdlemk7u-2N  42039  cdlemk11u-2N  42040  cdlemk12u-2N  42041  cdlemk21-2N  42042  cdlemk20-2N  42043  cdlemkuel-3  42049  cdlemkuv2-3N  42050  cdlemk22-3  42052  cdlemk33N  42060  cdlemk47  42100  cdlemk48  42101  cdlemk49  42102  cdlemk50  42103  cdlemk51  42104  cdlemk52  42105  cdlemk53a  42106  cdlemk55b  42111  cdlemkyyN  42113  cdlemk55u1  42116  cdlemk39u1  42118  cdlemk56  42122  dihord1  42369  dihord2a  42370  dihord10  42374  dihord11c  42375  dihord4  42409  dihord5apre  42413  dihglblem2N  42445  dihglbcpreN  42451  dihmeetlem3N  42456  dihjatc1  42462  dihjatc2N  42463  dihjatc3  42464  mapdpglem24  42855  baerlem3lem2  42861  baerlem5alem2  42862  baerlem5blem2  42863  hdmap14lem11  43029  hdmap14lem12  43030  hdmapglem7  43080  mzpsubst  43853  congmul  44068  congsub  44071  ntrclsiso  45161  ntrclskb  45163  ntrclsk3  45164  limsupre  46745  0ellimcdiv  46753  limclner  46755  sge0xaddlem2  47538  clnbgr3stgrgrlim  49211  gpgedgvtx1  49254  lincdifsn  49630  itschlc0yqe  49966  itscnhlc0xyqsol  49971