Theorem simp12 1205

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp112  1304  simp212  1313  simp312  1322  dvdsgcd  16473  coprimeprodsq  16738  pythagtriplem4  16749  pythagtriplem13  16757  pythagtriplem14  16758  pythagtriplem16  16760  pythagtrip  16764  pceu  16776  mremre  17524  lsmpropd  19574  m2cpminvid  22656  decpmatid  22673  mply1topmatcllem  22706  cmpsublem  23302  isfil2  23759  cxple2a  26624  isosctr  26747  nolesgn2o  27599  nolesgn2ores  27600  nogesgn1o  27601  nogesgn1ores  27602  nolt02o  27623  nogt01o  27624  sslttr  27736  cofsslt  27849  coinitsslt  27850  cofcut2  27853  onsfi  28270  brbtwn2  28868  colinearalg  28873  ax5seg  28901  axcontlem4  28930  bayesth  34406  bnj1204  34978  bnj1279  34984  ofscom  35980  btwndiff  36000  ifscgr  36017  brofs2  36050  brifs2  36051  fscgr  36053  btwnconn1lem1  36060  btwnconn1lem2  36061  btwnconn1lem3  36062  btwnconn1lem4  36063  btwnconn1lem12  36071  seglecgr12im  36083  seglecgr12  36084  ivthALT  36308  islshpcv  39031  lkrshp  39083  lshpsmreu  39087  lshpkrlem5  39092  cvrval3  39392  4noncolr3  39432  4noncolr2  39433  4noncolr1  39434  athgt  39435  3dimlem2  39438  3dimlem3a  39439  3dimlem4a  39442  3dimlem4  39443  3dimlem4OLDN  39444  1cvratex  39452  hlatexch4  39460  ps-2b  39461  3atlem4  39465  llnnleat  39492  2atm  39506  ps-2c  39507  llnmlplnN  39518  lplnnlelln  39522  2atmat  39540  lvoli2  39560  lvolnlelln  39563  4atlem3b  39577  4atlem10  39585  4atlem11a  39586  4atlem11b  39587  4atlem12a  39589  lplncvrlvol2  39594  2lplnja  39598  dalemswapyz  39635  lneq2at  39757  2lnat  39763  cdlema1N  39770  cdlemb  39773  paddasslem15  39813  pmodlem1  39825  llnmod2i2  39842  llnexchb2lem  39847  dalawlem1  39850  dalawlem3  39852  dalawlem4  39853  dalawlem6  39855  dalawlem7  39856  dalawlem9  39858  dalawlem10  39859  dalawlem11  39860  dalawlem12  39861  dalawlem13  39862  dalawlem15  39864  osumcllem5N  39939  osumcllem6N  39940  osumcllem7N  39941  osumcllem9N  39943  osumcllem10N  39944  osumcllem11N  39945  pl42lem1N  39958  lhpmcvr5N  40006  lhp2atne  40013  lhp2at0ne  40015  4atexlempw  40028  4atexlemex6  40053  4atexlem7  40054  ldilco  40095  ltrneq  40128  trlval2  40142  trlnidat  40152  cdlemd7  40183  cdleme7aa  40221  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme11c  40240  cdleme11e  40242  cdleme11l  40248  cdleme11  40249  cdleme14  40252  cdleme15a  40253  cdleme15c  40255  cdleme16b  40258  cdleme16c  40259  cdleme16d  40260  cdleme16e  40261  cdleme16f  40262  cdleme0nex  40269  cdleme18d  40274  cdleme19b  40283  cdleme19d  40285  cdleme19e  40286  cdleme20f  40293  cdleme20k  40298  cdleme20l1  40299  cdleme20l2  40300  cdleme20l  40301  cdleme20m  40302  cdleme21a  40304  cdleme21b  40305  cdleme21ct  40308  cdleme21d  40309  cdleme21e  40310  cdleme21f  40311  cdleme21h  40313  cdleme21i  40314  cdleme22eALTN  40324  cdleme22f2  40326  cdleme22g  40327  cdleme24  40331  cdleme25a  40332  cdleme25c  40334  cdleme25dN  40335  cdleme26e  40338  cdleme26ee  40339  cdleme26eALTN  40340  cdleme27N  40348  cdleme28a  40349  cdleme28b  40350  cdleme28  40352  cdlemefr32sn2aw  40383  cdlemefs32sn1aw  40393  cdleme43fsv1snlem  40399  cdleme41sn3a  40412  cdleme32c  40422  cdleme32e  40424  cdleme32le  40426  cdleme35a  40427  cdleme35b  40429  cdleme35c  40430  cdleme35e  40432  cdleme35f  40433  cdleme36a  40439  cdleme36m  40440  cdleme39a  40444  cdleme40m  40446  cdleme40n  40447  cdleme43bN  40469  cdleme43dN  40471  cdleme46f2g2  40472  cdleme46f2g1  40473  cdleme17d2  40474  cdleme4gfv  40486  cdlemeg49le  40490  cdlemeg46c  40492  cdlemeg46fvaw  40495  cdlemeg46nlpq  40496  cdlemeg46gfre  40511  cdleme50trn2  40530  cdleme  40539  cdlemg2idN  40575  cdlemg7fvbwN  40586  cdlemg10bALTN  40615  cdlemg10a  40619  cdlemg12d  40625  cdlemg12g  40628  cdlemg12  40629  cdlemg13a  40630  cdlemg13  40631  cdlemg17b  40641  cdlemg17dN  40642  cdlemg17dALTN  40643  cdlemg17e  40644  cdlemg17f  40645  cdlemg17i  40648  cdlemg17pq  40651  cdlemg17bq  40652  cdlemg17iqN  40653  cdlemg18d  40660  cdlemg18  40661  cdlemg19a  40662  cdlemg19  40663  cdlemg21  40665  cdlemg27a  40671  cdlemg28a  40672  cdlemg31b0N  40673  cdlemg27b  40675  cdlemg31c  40678  cdlemg33b0  40680  cdlemg33c0  40681  cdlemg28  40683  cdlemg33a  40685  cdlemg33  40690  cdlemg36  40693  ltrnco  40698  cdlemg44  40712  cdlemg47  40715  tendococl  40751  tendoplcl  40760  cdlemh1  40794  cdlemh2  40795  cdlemh  40796  cdlemi  40799  tendocan  40803  cdlemk5  40815  cdlemk6  40816  cdlemk7  40827  cdlemk11  40828  cdlemk12  40829  cdlemkole  40832  cdlemk14  40833  cdlemk15  40834  cdlemk16a  40835  cdlemk16  40836  cdlemk18  40847  cdlemk19  40848  cdlemk7u  40849  cdlemk11u  40850  cdlemk12u  40851  cdlemk21N  40852  cdlemk20  40853  cdlemkoatnle-2N  40854  cdlemk13-2N  40855  cdlemkole-2N  40856  cdlemk14-2N  40857  cdlemk15-2N  40858  cdlemk16-2N  40859  cdlemk17-2N  40860  cdlemk18-2N  40865  cdlemk19-2N  40866  cdlemk7u-2N  40867  cdlemk11u-2N  40868  cdlemk12u-2N  40869  cdlemk21-2N  40870  cdlemk20-2N  40871  cdlemk22  40872  cdlemk27-3  40886  cdlemk33N  40888  cdlemk11ta  40908  cdlemkid3N  40912  cdlemk11tc  40924  cdlemk11t  40925  cdlemk45  40926  cdlemk46  40927  cdlemk47  40928  cdlemk48  40929  cdlemk49  40930  cdlemk50  40931  cdlemk51  40932  cdlemk52  40933  cdlemk53a  40934  cdlemk55b  40939  cdlemkyyN  40941  cdlemk55u1  40944  cdlemk39u1  40946  cdlemk56  40950  cdlemm10N  41097  dihord1  41197  dihord2a  41198  dihord2b  41199  dihord10  41202  dihord4  41237  dihord5apre  41241  dihglblem2N  41273  dihjatc1  41290  dihjatc2N  41291  dihjatc3  41292  dihmeetlem15N  41300  dihmeetlem20N  41305  mapdpglem24  41683  hdmap14lem11  41857  hdmap14lem12  41858  flt4lem5  42623  mzpsubst  42721  monotuz  42914  congmul  42940  congsub  42943  ntrclsiso  44040  ntrclskb  44042  ntrclsk3  44043  infleinf  45352  mullimc  45598  mullimcf  45605  0ellimcdiv  45631  limclner  45633  sge0xaddlem2  46416  isubgr3stgrlem3  47953  lincdifsn  48410  itschlc0yqe  48746  itscnhlc0xyqsol  48751  itsclc0xyqsolr  48755  itsclquadeu  48763