Theorem simp13 1093

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

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpl13  1138  simpr13  1147  simp113  1192  simp213  1201  simp313  1210  funtpgOLD  5943  omeu  7665  ackbij1lem16  9057  dvdsgcd  15261  coprimeprodsq  15513  pythagtriplem4  15524  pythagtriplem13  15532  pythagtriplem14  15533  pythagtriplem16  15535  pythagtrip  15539  lsmpropd  18090  matsc  20256  mdetunilem7  20424  smadiadetglem2  20478  m2cpminvid  20558  pmatcollpw1lem1  20579  mp2pm2mplem2  20612  isfil2  21660  filuni  21689  ufprim  21713  cxple2a  24445  isosctr  24551  brbtwn2  25785  colinearalg  25790  ax5seg  25818  axcontlem4  25847  measres  30285  bayesth  30501  nolesgn2o  31824  ofscom  32114  btwndiff  32134  ifscgr  32151  brofs2  32184  brifs2  32185  fscgr  32187  btwnconn1lem1  32194  btwnconn1lem2  32195  btwnconn1lem3  32196  btwnconn1lem4  32197  btwnconn1lem12  32205  seglecgr12im  32217  seglecgr12  32218  ivthALT  32330  islshpcv  34340  eqlkr  34386  lshpsmreu  34396  lshpkrlem5  34401  atlrelat1  34608  cvlcvr1  34626  cvlcvrp  34627  cvlatcvr1  34628  cvlatcvr2  34629  4noncolr3  34739  4noncolr2  34740  4noncolr1  34741  athgt  34742  3dimlem2  34745  3dimlem3a  34746  3dimlem4a  34749  3dimlem4  34750  3dimlem4OLDN  34751  3dim1  34753  3dim2  34754  hlatexch4  34767  ps-2b  34768  3atlem6  34774  llnnleat  34799  2atm  34813  ps-2c  34814  llnmlplnN  34825  2atmat  34847  2llnjN  34853  lvoli2  34867  4atlem3b  34884  4atlem10  34892  4atlem11a  34893  4atlem11b  34894  4atlem12a  34896  4atlem12b  34897  dalemswapyz  34942  lneq2at  35064  2lnat  35070  cdlema1N  35077  cdlemb  35080  pmodlem1  35132  llnmod2i2  35149  dalawlem1  35157  dalawlem3  35159  dalawlem4  35160  dalawlem6  35162  dalawlem9  35165  dalawlem10  35166  dalawlem11  35167  dalawlem12  35168  dalawlem13  35169  dalawlem15  35171  dalaw  35172  pclfinN  35186  osumcllem5N  35246  osumcllem6N  35247  osumcllem7N  35248  osumcllem9N  35250  osumcllem11N  35252  pl42lem1N  35265  lhp2at0  35318  lhp2atne  35320  lhp2at0ne  35322  4atexlem7  35361  ldilco  35402  ltrneq  35435  cdlemd2  35486  cdleme0ex2N  35511  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7ga  35535  cdleme11c  35548  cdleme11l  35556  cdleme11  35557  cdleme14  35560  cdleme15a  35561  cdleme15c  35563  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme0nex  35577  cdleme19b  35592  cdleme19d  35594  cdleme19e  35595  cdleme20f  35602  cdleme20k  35607  cdleme20l1  35608  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme21a  35613  cdleme21b  35614  cdleme21c  35615  cdleme21ct  35617  cdleme21d  35618  cdleme21e  35619  cdleme21f  35620  cdleme21i  35623  cdleme22cN  35630  cdleme22eALTN  35633  cdleme25a  35641  cdleme25c  35643  cdleme25dN  35644  cdleme26e  35647  cdleme26ee  35648  cdleme26eALTN  35649  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme28a  35658  cdleme28b  35659  cdleme28  35661  cdlemefr32sn2aw  35692  cdlemefs32sn1aw  35702  cdleme43fsv1snlem  35708  cdleme41sn3a  35721  cdleme32c  35731  cdleme32e  35733  cdleme32le  35735  cdleme35a  35736  cdleme35b  35738  cdleme35d  35740  cdleme36a  35748  cdleme36m  35749  cdleme39a  35753  cdleme40m  35755  cdleme40n  35756  cdleme43bN  35778  cdleme43dN  35780  cdleme46f2g2  35781  cdleme46f2g1  35782  cdleme4gfv  35795  cdlemeg49le  35799  cdlemeg46c  35801  cdlemeg46fvaw  35804  cdlemeg46nlpq  35805  cdlemeg46gfre  35820  cdleme50trn2  35839  cdlemg2ce  35880  cdlemg2idN  35884  cdlemg7fvbwN  35895  cdlemg10bALTN  35924  cdlemg10a  35928  cdlemg12d  35934  cdlemg12g  35937  cdlemg12  35938  cdlemg13a  35939  cdlemg13  35940  cdlemg17b  35950  cdlemg17dN  35951  cdlemg17dALTN  35952  cdlemg17e  35953  cdlemg17pq  35960  cdlemg17bq  35961  cdlemg18d  35969  cdlemg19a  35971  cdlemg19  35972  cdlemg21  35974  cdlemg27a  35980  cdlemg31b0N  35982  cdlemg27b  35984  cdlemg31c  35987  cdlemg33b0  35989  cdlemg33c0  35990  cdlemg28b  35991  cdlemg33a  35994  cdlemg33  35999  ltrnco  36007  cdlemg44  36021  cdlemg47  36024  tendococl  36060  tendoplcl  36069  cdlemh1  36103  cdlemh2  36104  cdlemh  36105  cdlemi  36108  cdlemk5  36124  cdlemk6  36125  cdlemksel  36133  cdlemksv2  36135  cdlemk7  36136  cdlemk11  36137  cdlemk12  36138  cdlemkole  36141  cdlemk14  36142  cdlemk15  36143  cdlemk16a  36144  cdlemk16  36145  cdlemk1u  36147  cdlemk5u  36149  cdlemk6u  36150  cdlemkuel  36153  cdlemkuv2  36155  cdlemk18  36156  cdlemk19  36157  cdlemk7u  36158  cdlemk11u  36159  cdlemk12u  36160  cdlemk21N  36161  cdlemk20  36162  cdlemkoatnle-2N  36163  cdlemk13-2N  36164  cdlemkole-2N  36165  cdlemk14-2N  36166  cdlemk15-2N  36167  cdlemk16-2N  36168  cdlemk17-2N  36169  cdlemk18-2N  36174  cdlemk19-2N  36175  cdlemk7u-2N  36176  cdlemk11u-2N  36177  cdlemk12u-2N  36178  cdlemk21-2N  36179  cdlemk20-2N  36180  cdlemkuel-3  36186  cdlemkuv2-3N  36187  cdlemk22-3  36189  cdlemk33N  36197  cdlemk47  36237  cdlemk48  36238  cdlemk49  36239  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  cdlemk53a  36243  cdlemk55b  36248  cdlemkyyN  36250  cdlemk55u1  36253  cdlemk39u1  36255  cdlemk56  36259  dihord1  36507  dihord2a  36508  dihord10  36512  dihord11c  36513  dihord4  36547  dihord5apre  36551  dihglblem2N  36583  dihglbcpreN  36589  dihmeetlem3N  36594  dihjatc1  36600  dihjatc2N  36601  dihjatc3  36602  mapdpglem24  36993  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  hdmap14lem11  37170  hdmap14lem12  37171  hdmapglem7  37221  mzpsubst  37311  congmul  37534  congsub  37537  ntrclsiso  38365  ntrclskb  38367  ntrclsk3  38368  limsupre  39873  0ellimcdiv  39881  limclner  39883  sge0xaddlem2  40651  lincdifsn  42213