Theorem simp12 1267

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp12	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Proof of Theorem simp12

Step	Hyp	Ref	Expression
1		simp2 1173	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	3ad2ant1 1169	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  simpl12OLD  1338  simpr12OLD  1356  simp112  1408  simp212  1417  simp312  1426  dvdsgcd  15635  coprimeprodsq  15885  pythagtriplem4  15896  pythagtriplem13  15904  pythagtriplem14  15905  pythagtriplem16  15907  pythagtrip  15911  pceu  15923  mremre  16618  lsmpropd  18442  m2cpminvid  20929  decpmatid  20946  mply1topmatcllem  20979  cmpsublem  21574  isfil2  22031  cxple2a  24845  isosctr  24962  brbtwn2  26205  colinearalg  26210  ax5seg  26238  axcontlem4  26267  bayesth  31048  bnj1204  31627  bnj1279  31633  nolesgn2o  32364  nolesgn2ores  32365  nolt02o  32385  ofscom  32654  btwndiff  32674  ifscgr  32691  brofs2  32724  brifs2  32725  fscgr  32727  btwnconn1lem1  32734  btwnconn1lem2  32735  btwnconn1lem3  32736  btwnconn1lem4  32737  btwnconn1lem12  32745  seglecgr12im  32757  seglecgr12  32758  ivthALT  32869  islshpcv  35129  lkrshp  35181  lshpsmreu  35185  lshpkrlem5  35190  cvrval3  35489  4noncolr3  35529  4noncolr2  35530  4noncolr1  35531  athgt  35532  3dimlem2  35535  3dimlem3a  35536  3dimlem4a  35539  3dimlem4  35540  3dimlem4OLDN  35541  1cvratex  35549  hlatexch4  35557  ps-2b  35558  3atlem4  35562  llnnleat  35589  2atm  35603  ps-2c  35604  llnmlplnN  35615  lplnnlelln  35619  2atmat  35637  lvoli2  35657  lvolnlelln  35660  4atlem3b  35674  4atlem10  35682  4atlem11a  35683  4atlem11b  35684  4atlem12a  35686  lplncvrlvol2  35691  2lplnja  35695  dalemswapyz  35732  lneq2at  35854  2lnat  35860  cdlema1N  35867  cdlemb  35870  paddasslem15  35910  pmodlem1  35922  llnmod2i2  35939  llnexchb2lem  35944  dalawlem1  35947  dalawlem3  35949  dalawlem4  35950  dalawlem6  35952  dalawlem7  35953  dalawlem9  35955  dalawlem10  35956  dalawlem11  35957  dalawlem12  35958  dalawlem13  35959  dalawlem15  35961  osumcllem5N  36036  osumcllem6N  36037  osumcllem7N  36038  osumcllem9N  36040  osumcllem10N  36041  osumcllem11N  36042  pl42lem1N  36055  lhpmcvr5N  36103  lhp2atne  36110  lhp2at0ne  36112  4atexlempw  36125  4atexlemex6  36150  4atexlem7  36151  ldilco  36192  ltrneq  36225  trlval2  36239  trlnidat  36249  cdlemd7  36280  cdleme7aa  36318  cdleme7c  36321  cdleme7d  36322  cdleme7e  36323  cdleme7ga  36324  cdleme7  36325  cdleme11c  36337  cdleme11e  36339  cdleme11l  36345  cdleme11  36346  cdleme14  36349  cdleme15a  36350  cdleme15c  36352  cdleme16b  36355  cdleme16c  36356  cdleme16d  36357  cdleme16e  36358  cdleme16f  36359  cdleme0nex  36366  cdleme18d  36371  cdleme19b  36380  cdleme19d  36382  cdleme19e  36383  cdleme20f  36390  cdleme20k  36395  cdleme20l1  36396  cdleme20l2  36397  cdleme20l  36398  cdleme20m  36399  cdleme21a  36401  cdleme21b  36402  cdleme21ct  36405  cdleme21d  36406  cdleme21e  36407  cdleme21f  36408  cdleme21h  36410  cdleme21i  36411  cdleme22eALTN  36421  cdleme22f2  36423  cdleme22g  36424  cdleme24  36428  cdleme25a  36429  cdleme25c  36431  cdleme25dN  36432  cdleme26e  36435  cdleme26ee  36436  cdleme26eALTN  36437  cdleme27N  36445  cdleme28a  36446  cdleme28b  36447  cdleme28  36449  cdlemefr32sn2aw  36480  cdlemefs32sn1aw  36490  cdleme43fsv1snlem  36496  cdleme41sn3a  36509  cdleme32c  36519  cdleme32e  36521  cdleme32le  36523  cdleme35a  36524  cdleme35b  36526  cdleme35c  36527  cdleme35e  36529  cdleme35f  36530  cdleme36a  36536  cdleme36m  36537  cdleme39a  36541  cdleme40m  36543  cdleme40n  36544  cdleme43bN  36566  cdleme43dN  36568  cdleme46f2g2  36569  cdleme46f2g1  36570  cdleme17d2  36571  cdleme4gfv  36583  cdlemeg49le  36587  cdlemeg46c  36589  cdlemeg46fvaw  36592  cdlemeg46nlpq  36593  cdlemeg46gfre  36608  cdleme50trn2  36627  cdleme  36636  cdlemg2idN  36672  cdlemg7fvbwN  36683  cdlemg10bALTN  36712  cdlemg10a  36716  cdlemg12d  36722  cdlemg12g  36725  cdlemg12  36726  cdlemg13a  36727  cdlemg13  36728  cdlemg17b  36738  cdlemg17dN  36739  cdlemg17dALTN  36740  cdlemg17e  36741  cdlemg17f  36742  cdlemg17i  36745  cdlemg17pq  36748  cdlemg17bq  36749  cdlemg17iqN  36750  cdlemg18d  36757  cdlemg18  36758  cdlemg19a  36759  cdlemg19  36760  cdlemg21  36762  cdlemg27a  36768  cdlemg28a  36769  cdlemg31b0N  36770  cdlemg27b  36772  cdlemg31c  36775  cdlemg33b0  36777  cdlemg33c0  36778  cdlemg28  36780  cdlemg33a  36782  cdlemg33  36787  cdlemg36  36790  ltrnco  36795  cdlemg44  36809  cdlemg47  36812  tendococl  36848  tendoplcl  36857  cdlemh1  36891  cdlemh2  36892  cdlemh  36893  cdlemi  36896  tendocan  36900  cdlemk5  36912  cdlemk6  36913  cdlemk7  36924  cdlemk11  36925  cdlemk12  36926  cdlemkole  36929  cdlemk14  36930  cdlemk15  36931  cdlemk16a  36932  cdlemk16  36933  cdlemk18  36944  cdlemk19  36945  cdlemk7u  36946  cdlemk11u  36947  cdlemk12u  36948  cdlemk21N  36949  cdlemk20  36950  cdlemkoatnle-2N  36951  cdlemk13-2N  36952  cdlemkole-2N  36953  cdlemk14-2N  36954  cdlemk15-2N  36955  cdlemk16-2N  36956  cdlemk17-2N  36957  cdlemk18-2N  36962  cdlemk19-2N  36963  cdlemk7u-2N  36964  cdlemk11u-2N  36965  cdlemk12u-2N  36966  cdlemk21-2N  36967  cdlemk20-2N  36968  cdlemk22  36969  cdlemk27-3  36983  cdlemk33N  36985  cdlemk11ta  37005  cdlemkid3N  37009  cdlemk11tc  37021  cdlemk11t  37022  cdlemk45  37023  cdlemk46  37024  cdlemk47  37025  cdlemk48  37026  cdlemk49  37027  cdlemk50  37028  cdlemk51  37029  cdlemk52  37030  cdlemk53a  37031  cdlemk55b  37036  cdlemkyyN  37038  cdlemk55u1  37041  cdlemk39u1  37043  cdlemk56  37047  cdlemm10N  37194  dihord1  37294  dihord2a  37295  dihord2b  37296  dihord10  37299  dihord4  37334  dihord5apre  37338  dihglblem2N  37370  dihjatc1  37387  dihjatc2N  37388  dihjatc3  37389  dihmeetlem15N  37397  dihmeetlem20N  37402  mapdpglem24  37780  hdmap14lem11  37954  hdmap14lem12  37955  mzpsubst  38156  monotuz  38350  congmul  38378  congsub  38381  ntrclsiso  39206  ntrclskb  39208  ntrclsk3  39209  infleinf  40386  mullimc  40644  mullimcf  40651  0ellimcdiv  40677  limclner  40679  sge0xaddlem2  41443  lincdifsn  43061  itsclc0lem5  43313