Theorem simp13 1201

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp113  1300  simp213  1309  simp313  1318  omeu  8213  ackbij1lem16  9659  dvdsgcd  15894  coprimeprodsq  16147  pythagtriplem4  16158  pythagtriplem13  16166  pythagtriplem14  16167  pythagtriplem16  16169  pythagtrip  16173  lsmpropd  18805  matsc  21061  mdetunilem7  21229  smadiadetglem2  21283  m2cpminvid  21363  pmatcollpw1lem1  21384  mp2pm2mplem2  21417  isfil2  22466  filuni  22495  ufprim  22519  cxple2a  25284  isosctr  25401  brbtwn2  26693  colinearalg  26698  ax5seg  26726  axcontlem4  26755  measres  31483  bayesth  31699  nolesgn2o  33180  ofscom  33470  btwndiff  33490  ifscgr  33507  brofs2  33540  brifs2  33541  fscgr  33543  btwnconn1lem1  33550  btwnconn1lem2  33551  btwnconn1lem3  33552  btwnconn1lem4  33553  btwnconn1lem12  33561  seglecgr12im  33573  seglecgr12  33574  ivthALT  33685  islshpcv  36191  eqlkr  36237  lshpsmreu  36247  lshpkrlem5  36252  atlrelat1  36459  cvlcvr1  36477  cvlcvrp  36478  cvlatcvr1  36479  cvlatcvr2  36480  4noncolr3  36591  4noncolr2  36592  4noncolr1  36593  athgt  36594  3dimlem2  36597  3dimlem3a  36598  3dimlem4a  36601  3dimlem4  36602  3dimlem4OLDN  36603  3dim1  36605  3dim2  36606  hlatexch4  36619  ps-2b  36620  3atlem6  36626  llnnleat  36651  2atm  36665  ps-2c  36666  llnmlplnN  36677  2atmat  36699  2llnjN  36705  lvoli2  36719  4atlem3b  36736  4atlem10  36744  4atlem11a  36745  4atlem11b  36746  4atlem12a  36748  4atlem12b  36749  dalemswapyz  36794  lneq2at  36916  2lnat  36922  cdlema1N  36929  cdlemb  36932  pmodlem1  36984  llnmod2i2  37001  dalawlem1  37009  dalawlem3  37011  dalawlem4  37012  dalawlem6  37014  dalawlem9  37017  dalawlem10  37018  dalawlem11  37019  dalawlem12  37020  dalawlem13  37021  dalawlem15  37023  dalaw  37024  pclfinN  37038  osumcllem5N  37098  osumcllem6N  37099  osumcllem7N  37100  osumcllem9N  37102  osumcllem11N  37104  pl42lem1N  37117  lhp2at0  37170  lhp2atne  37172  lhp2at0ne  37174  4atexlem7  37213  ldilco  37254  ltrneq  37287  cdlemd2  37337  cdleme0ex2N  37362  cdleme7aa  37380  cdleme7c  37383  cdleme7d  37384  cdleme7ga  37386  cdleme11c  37399  cdleme11l  37407  cdleme11  37408  cdleme14  37411  cdleme15a  37412  cdleme15c  37414  cdleme16b  37417  cdleme16c  37418  cdleme16d  37419  cdleme16e  37420  cdleme16f  37421  cdleme0nex  37428  cdleme19b  37442  cdleme19d  37444  cdleme19e  37445  cdleme20f  37452  cdleme20k  37457  cdleme20l1  37458  cdleme20l2  37459  cdleme20l  37460  cdleme20m  37461  cdleme21a  37463  cdleme21b  37464  cdleme21c  37465  cdleme21ct  37467  cdleme21d  37468  cdleme21e  37469  cdleme21f  37470  cdleme21i  37473  cdleme22cN  37480  cdleme22eALTN  37483  cdleme25a  37491  cdleme25c  37493  cdleme25dN  37494  cdleme26e  37497  cdleme26ee  37498  cdleme26eALTN  37499  cdleme26f2ALTN  37502  cdleme26f2  37503  cdleme28a  37508  cdleme28b  37509  cdleme28  37511  cdlemefr32sn2aw  37542  cdlemefs32sn1aw  37552  cdleme43fsv1snlem  37558  cdleme41sn3a  37571  cdleme32c  37581  cdleme32e  37583  cdleme32le  37585  cdleme35a  37586  cdleme35b  37588  cdleme35d  37590  cdleme36a  37598  cdleme36m  37599  cdleme39a  37603  cdleme40m  37605  cdleme40n  37606  cdleme43bN  37628  cdleme43dN  37630  cdleme46f2g2  37631  cdleme46f2g1  37632  cdleme4gfv  37645  cdlemeg49le  37649  cdlemeg46c  37651  cdlemeg46fvaw  37654  cdlemeg46nlpq  37655  cdlemeg46gfre  37670  cdleme50trn2  37689  cdlemg2ce  37730  cdlemg2idN  37734  cdlemg7fvbwN  37745  cdlemg10bALTN  37774  cdlemg10a  37778  cdlemg12d  37784  cdlemg12g  37787  cdlemg12  37788  cdlemg13a  37789  cdlemg13  37790  cdlemg17b  37800  cdlemg17dN  37801  cdlemg17dALTN  37802  cdlemg17e  37803  cdlemg17pq  37810  cdlemg17bq  37811  cdlemg18d  37819  cdlemg19a  37821  cdlemg19  37822  cdlemg21  37824  cdlemg27a  37830  cdlemg31b0N  37832  cdlemg27b  37834  cdlemg31c  37837  cdlemg33b0  37839  cdlemg33c0  37840  cdlemg28b  37841  cdlemg33a  37844  cdlemg33  37849  ltrnco  37857  cdlemg44  37871  cdlemg47  37874  tendococl  37910  tendoplcl  37919  cdlemh1  37953  cdlemh2  37954  cdlemh  37955  cdlemi  37958  cdlemk5  37974  cdlemk6  37975  cdlemksel  37983  cdlemksv2  37985  cdlemk7  37986  cdlemk11  37987  cdlemk12  37988  cdlemkole  37991  cdlemk14  37992  cdlemk15  37993  cdlemk16a  37994  cdlemk16  37995  cdlemk1u  37997  cdlemk5u  37999  cdlemk6u  38000  cdlemkuel  38003  cdlemkuv2  38005  cdlemk18  38006  cdlemk19  38007  cdlemk7u  38008  cdlemk11u  38009  cdlemk12u  38010  cdlemk21N  38011  cdlemk20  38012  cdlemkoatnle-2N  38013  cdlemk13-2N  38014  cdlemkole-2N  38015  cdlemk14-2N  38016  cdlemk15-2N  38017  cdlemk16-2N  38018  cdlemk17-2N  38019  cdlemk18-2N  38024  cdlemk19-2N  38025  cdlemk7u-2N  38026  cdlemk11u-2N  38027  cdlemk12u-2N  38028  cdlemk21-2N  38029  cdlemk20-2N  38030  cdlemkuel-3  38036  cdlemkuv2-3N  38037  cdlemk22-3  38039  cdlemk33N  38047  cdlemk47  38087  cdlemk48  38088  cdlemk49  38089  cdlemk50  38090  cdlemk51  38091  cdlemk52  38092  cdlemk53a  38093  cdlemk55b  38098  cdlemkyyN  38100  cdlemk55u1  38103  cdlemk39u1  38105  cdlemk56  38109  dihord1  38356  dihord2a  38357  dihord10  38361  dihord11c  38362  dihord4  38396  dihord5apre  38400  dihglblem2N  38432  dihglbcpreN  38438  dihmeetlem3N  38443  dihjatc1  38449  dihjatc2N  38450  dihjatc3  38451  mapdpglem24  38842  baerlem3lem2  38848  baerlem5alem2  38849  baerlem5blem2  38850  hdmap14lem11  39016  hdmap14lem12  39017  hdmapglem7  39067  mzpsubst  39352  congmul  39571  congsub  39574  ntrclsiso  40424  ntrclskb  40426  ntrclsk3  40427  limsupre  41929  0ellimcdiv  41937  limclner  41939  sge0xaddlem2  42723  lincdifsn  44486  itschlc0yqe  44754  itscnhlc0xyqsol  44759