Theorem simp13 1206

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  simp113  1305  simp213  1314  simp313  1323  omeu  8582  ackbij1lem16  10227  dvdsgcd  16483  coprimeprodsq  16738  pythagtriplem4  16749  pythagtriplem13  16757  pythagtriplem14  16758  pythagtriplem16  16760  pythagtrip  16764  lsmpropd  19540  matsc  21944  mdetunilem7  22112  smadiadetglem2  22166  m2cpminvid  22247  pmatcollpw1lem1  22268  mp2pm2mplem2  22301  isfil2  23352  filuni  23381  ufprim  23405  cxple2a  26199  isosctr  26316  nolesgn2o  27164  nogesgn1o  27166  sslttr  27298  cofcut2  27399  brbtwn2  28153  colinearalg  28158  ax5seg  28186  axcontlem4  28215  measres  33209  bayesth  33427  ofscom  34968  btwndiff  34988  ifscgr  35005  brofs2  35038  brifs2  35039  fscgr  35041  btwnconn1lem1  35048  btwnconn1lem2  35049  btwnconn1lem3  35050  btwnconn1lem4  35051  btwnconn1lem12  35059  seglecgr12im  35071  seglecgr12  35072  ivthALT  35209  islshpcv  37912  eqlkr  37958  lshpsmreu  37968  lshpkrlem5  37973  atlrelat1  38180  cvlcvr1  38198  cvlcvrp  38199  cvlatcvr1  38200  cvlatcvr2  38201  4noncolr3  38313  4noncolr2  38314  4noncolr1  38315  athgt  38316  3dimlem2  38319  3dimlem3a  38320  3dimlem4a  38323  3dimlem4  38324  3dimlem4OLDN  38325  3dim1  38327  3dim2  38328  hlatexch4  38341  ps-2b  38342  3atlem6  38348  llnnleat  38373  2atm  38387  ps-2c  38388  llnmlplnN  38399  2atmat  38421  2llnjN  38427  lvoli2  38441  4atlem3b  38458  4atlem10  38466  4atlem11a  38467  4atlem11b  38468  4atlem12a  38470  4atlem12b  38471  dalemswapyz  38516  lneq2at  38638  2lnat  38644  cdlema1N  38651  cdlemb  38654  pmodlem1  38706  llnmod2i2  38723  dalawlem1  38731  dalawlem3  38733  dalawlem4  38734  dalawlem6  38736  dalawlem9  38739  dalawlem10  38740  dalawlem11  38741  dalawlem12  38742  dalawlem13  38743  dalawlem15  38745  dalaw  38746  pclfinN  38760  osumcllem5N  38820  osumcllem6N  38821  osumcllem7N  38822  osumcllem9N  38824  osumcllem11N  38826  pl42lem1N  38839  lhp2at0  38892  lhp2atne  38894  lhp2at0ne  38896  4atexlem7  38935  ldilco  38976  ltrneq  39009  cdlemd2  39059  cdleme0ex2N  39084  cdleme7aa  39102  cdleme7c  39105  cdleme7d  39106  cdleme7ga  39108  cdleme11c  39121  cdleme11l  39129  cdleme11  39130  cdleme14  39133  cdleme15a  39134  cdleme15c  39136  cdleme16b  39139  cdleme16c  39140  cdleme16d  39141  cdleme16e  39142  cdleme16f  39143  cdleme0nex  39150  cdleme19b  39164  cdleme19d  39166  cdleme19e  39167  cdleme20f  39174  cdleme20k  39179  cdleme20l1  39180  cdleme20l2  39181  cdleme20l  39182  cdleme20m  39183  cdleme21a  39185  cdleme21b  39186  cdleme21c  39187  cdleme21ct  39189  cdleme21d  39190  cdleme21e  39191  cdleme21f  39192  cdleme21i  39195  cdleme22cN  39202  cdleme22eALTN  39205  cdleme25a  39213  cdleme25c  39215  cdleme25dN  39216  cdleme26e  39219  cdleme26ee  39220  cdleme26eALTN  39221  cdleme26f2ALTN  39224  cdleme26f2  39225  cdleme28a  39230  cdleme28b  39231  cdleme28  39233  cdlemefr32sn2aw  39264  cdlemefs32sn1aw  39274  cdleme43fsv1snlem  39280  cdleme41sn3a  39293  cdleme32c  39303  cdleme32e  39305  cdleme32le  39307  cdleme35a  39308  cdleme35b  39310  cdleme35d  39312  cdleme36a  39320  cdleme36m  39321  cdleme39a  39325  cdleme40m  39327  cdleme40n  39328  cdleme43bN  39350  cdleme43dN  39352  cdleme46f2g2  39353  cdleme46f2g1  39354  cdleme4gfv  39367  cdlemeg49le  39371  cdlemeg46c  39373  cdlemeg46fvaw  39376  cdlemeg46nlpq  39377  cdlemeg46gfre  39392  cdleme50trn2  39411  cdlemg2ce  39452  cdlemg2idN  39456  cdlemg7fvbwN  39467  cdlemg10bALTN  39496  cdlemg10a  39500  cdlemg12d  39506  cdlemg12g  39509  cdlemg12  39510  cdlemg13a  39511  cdlemg13  39512  cdlemg17b  39522  cdlemg17dN  39523  cdlemg17dALTN  39524  cdlemg17e  39525  cdlemg17pq  39532  cdlemg17bq  39533  cdlemg18d  39541  cdlemg19a  39543  cdlemg19  39544  cdlemg21  39546  cdlemg27a  39552  cdlemg31b0N  39554  cdlemg27b  39556  cdlemg31c  39559  cdlemg33b0  39561  cdlemg33c0  39562  cdlemg28b  39563  cdlemg33a  39566  cdlemg33  39571  ltrnco  39579  cdlemg44  39593  cdlemg47  39596  tendococl  39632  tendoplcl  39641  cdlemh1  39675  cdlemh2  39676  cdlemh  39677  cdlemi  39680  cdlemk5  39696  cdlemk6  39697  cdlemksel  39705  cdlemksv2  39707  cdlemk7  39708  cdlemk11  39709  cdlemk12  39710  cdlemkole  39713  cdlemk14  39714  cdlemk15  39715  cdlemk16a  39716  cdlemk16  39717  cdlemk1u  39719  cdlemk5u  39721  cdlemk6u  39722  cdlemkuel  39725  cdlemkuv2  39727  cdlemk18  39728  cdlemk19  39729  cdlemk7u  39730  cdlemk11u  39731  cdlemk12u  39732  cdlemk21N  39733  cdlemk20  39734  cdlemkoatnle-2N  39735  cdlemk13-2N  39736  cdlemkole-2N  39737  cdlemk14-2N  39738  cdlemk15-2N  39739  cdlemk16-2N  39740  cdlemk17-2N  39741  cdlemk18-2N  39746  cdlemk19-2N  39747  cdlemk7u-2N  39748  cdlemk11u-2N  39749  cdlemk12u-2N  39750  cdlemk21-2N  39751  cdlemk20-2N  39752  cdlemkuel-3  39758  cdlemkuv2-3N  39759  cdlemk22-3  39761  cdlemk33N  39769  cdlemk47  39809  cdlemk48  39810  cdlemk49  39811  cdlemk50  39812  cdlemk51  39813  cdlemk52  39814  cdlemk53a  39815  cdlemk55b  39820  cdlemkyyN  39822  cdlemk55u1  39825  cdlemk39u1  39827  cdlemk56  39831  dihord1  40078  dihord2a  40079  dihord10  40083  dihord11c  40084  dihord4  40118  dihord5apre  40122  dihglblem2N  40154  dihglbcpreN  40160  dihmeetlem3N  40165  dihjatc1  40171  dihjatc2N  40172  dihjatc3  40173  mapdpglem24  40564  baerlem3lem2  40570  baerlem5alem2  40571  baerlem5blem2  40572  hdmap14lem11  40738  hdmap14lem12  40739  hdmapglem7  40789  mzpsubst  41472  congmul  41692  congsub  41695  ntrclsiso  42804  ntrclskb  42806  ntrclsk3  42807  limsupre  44344  0ellimcdiv  44352  limclner  44354  sge0xaddlem2  45137  lincdifsn  47059  itschlc0yqe  47400  itscnhlc0xyqsol  47405