Theorem simp12 1201

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  simp112  1300  simp212  1309  simp312  1318  dvdsgcd  16523  coprimeprodsq  16780  pythagtriplem4  16791  pythagtriplem13  16799  pythagtriplem14  16800  pythagtriplem16  16802  pythagtrip  16806  pceu  16818  mremre  17587  lsmpropd  19644  m2cpminvid  22699  decpmatid  22716  mply1topmatcllem  22749  cmpsublem  23347  isfil2  23804  cxple2a  26678  isosctr  26798  nolesgn2o  27650  nolesgn2ores  27651  nogesgn1o  27652  nogesgn1ores  27653  nolt02o  27674  nogt01o  27675  sslttr  27786  cofsslt  27884  coinitsslt  27885  cofcut2  27888  brbtwn2  28788  colinearalg  28793  ax5seg  28821  axcontlem4  28850  bayesth  34190  bnj1204  34774  bnj1279  34780  ofscom  35734  btwndiff  35754  ifscgr  35771  brofs2  35804  brifs2  35805  fscgr  35807  btwnconn1lem1  35814  btwnconn1lem2  35815  btwnconn1lem3  35816  btwnconn1lem4  35817  btwnconn1lem12  35825  seglecgr12im  35837  seglecgr12  35838  ivthALT  35950  islshpcv  38655  lkrshp  38707  lshpsmreu  38711  lshpkrlem5  38716  cvrval3  39016  4noncolr3  39056  4noncolr2  39057  4noncolr1  39058  athgt  39059  3dimlem2  39062  3dimlem3a  39063  3dimlem4a  39066  3dimlem4  39067  3dimlem4OLDN  39068  1cvratex  39076  hlatexch4  39084  ps-2b  39085  3atlem4  39089  llnnleat  39116  2atm  39130  ps-2c  39131  llnmlplnN  39142  lplnnlelln  39146  2atmat  39164  lvoli2  39184  lvolnlelln  39187  4atlem3b  39201  4atlem10  39209  4atlem11a  39210  4atlem11b  39211  4atlem12a  39213  lplncvrlvol2  39218  2lplnja  39222  dalemswapyz  39259  lneq2at  39381  2lnat  39387  cdlema1N  39394  cdlemb  39397  paddasslem15  39437  pmodlem1  39449  llnmod2i2  39466  llnexchb2lem  39471  dalawlem1  39474  dalawlem3  39476  dalawlem4  39477  dalawlem6  39479  dalawlem7  39480  dalawlem9  39482  dalawlem10  39483  dalawlem11  39484  dalawlem12  39485  dalawlem13  39486  dalawlem15  39488  osumcllem5N  39563  osumcllem6N  39564  osumcllem7N  39565  osumcllem9N  39567  osumcllem10N  39568  osumcllem11N  39569  pl42lem1N  39582  lhpmcvr5N  39630  lhp2atne  39637  lhp2at0ne  39639  4atexlempw  39652  4atexlemex6  39677  4atexlem7  39678  ldilco  39719  ltrneq  39752  trlval2  39766  trlnidat  39776  cdlemd7  39807  cdleme7aa  39845  cdleme7c  39848  cdleme7d  39849  cdleme7e  39850  cdleme7ga  39851  cdleme7  39852  cdleme11c  39864  cdleme11e  39866  cdleme11l  39872  cdleme11  39873  cdleme14  39876  cdleme15a  39877  cdleme15c  39879  cdleme16b  39882  cdleme16c  39883  cdleme16d  39884  cdleme16e  39885  cdleme16f  39886  cdleme0nex  39893  cdleme18d  39898  cdleme19b  39907  cdleme19d  39909  cdleme19e  39910  cdleme20f  39917  cdleme20k  39922  cdleme20l1  39923  cdleme20l2  39924  cdleme20l  39925  cdleme20m  39926  cdleme21a  39928  cdleme21b  39929  cdleme21ct  39932  cdleme21d  39933  cdleme21e  39934  cdleme21f  39935  cdleme21h  39937  cdleme21i  39938  cdleme22eALTN  39948  cdleme22f2  39950  cdleme22g  39951  cdleme24  39955  cdleme25a  39956  cdleme25c  39958  cdleme25dN  39959  cdleme26e  39962  cdleme26ee  39963  cdleme26eALTN  39964  cdleme27N  39972  cdleme28a  39973  cdleme28b  39974  cdleme28  39976  cdlemefr32sn2aw  40007  cdlemefs32sn1aw  40017  cdleme43fsv1snlem  40023  cdleme41sn3a  40036  cdleme32c  40046  cdleme32e  40048  cdleme32le  40050  cdleme35a  40051  cdleme35b  40053  cdleme35c  40054  cdleme35e  40056  cdleme35f  40057  cdleme36a  40063  cdleme36m  40064  cdleme39a  40068  cdleme40m  40070  cdleme40n  40071  cdleme43bN  40093  cdleme43dN  40095  cdleme46f2g2  40096  cdleme46f2g1  40097  cdleme17d2  40098  cdleme4gfv  40110  cdlemeg49le  40114  cdlemeg46c  40116  cdlemeg46fvaw  40119  cdlemeg46nlpq  40120  cdlemeg46gfre  40135  cdleme50trn2  40154  cdleme  40163  cdlemg2idN  40199  cdlemg7fvbwN  40210  cdlemg10bALTN  40239  cdlemg10a  40243  cdlemg12d  40249  cdlemg12g  40252  cdlemg12  40253  cdlemg13a  40254  cdlemg13  40255  cdlemg17b  40265  cdlemg17dN  40266  cdlemg17dALTN  40267  cdlemg17e  40268  cdlemg17f  40269  cdlemg17i  40272  cdlemg17pq  40275  cdlemg17bq  40276  cdlemg17iqN  40277  cdlemg18d  40284  cdlemg18  40285  cdlemg19a  40286  cdlemg19  40287  cdlemg21  40289  cdlemg27a  40295  cdlemg28a  40296  cdlemg31b0N  40297  cdlemg27b  40299  cdlemg31c  40302  cdlemg33b0  40304  cdlemg33c0  40305  cdlemg28  40307  cdlemg33a  40309  cdlemg33  40314  cdlemg36  40317  ltrnco  40322  cdlemg44  40336  cdlemg47  40339  tendococl  40375  tendoplcl  40384  cdlemh1  40418  cdlemh2  40419  cdlemh  40420  cdlemi  40423  tendocan  40427  cdlemk5  40439  cdlemk6  40440  cdlemk7  40451  cdlemk11  40452  cdlemk12  40453  cdlemkole  40456  cdlemk14  40457  cdlemk15  40458  cdlemk16a  40459  cdlemk16  40460  cdlemk18  40471  cdlemk19  40472  cdlemk7u  40473  cdlemk11u  40474  cdlemk12u  40475  cdlemk21N  40476  cdlemk20  40477  cdlemkoatnle-2N  40478  cdlemk13-2N  40479  cdlemkole-2N  40480  cdlemk14-2N  40481  cdlemk15-2N  40482  cdlemk16-2N  40483  cdlemk17-2N  40484  cdlemk18-2N  40489  cdlemk19-2N  40490  cdlemk7u-2N  40491  cdlemk11u-2N  40492  cdlemk12u-2N  40493  cdlemk21-2N  40494  cdlemk20-2N  40495  cdlemk22  40496  cdlemk27-3  40510  cdlemk33N  40512  cdlemk11ta  40532  cdlemkid3N  40536  cdlemk11tc  40548  cdlemk11t  40549  cdlemk45  40550  cdlemk46  40551  cdlemk47  40552  cdlemk48  40553  cdlemk49  40554  cdlemk50  40555  cdlemk51  40556  cdlemk52  40557  cdlemk53a  40558  cdlemk55b  40563  cdlemkyyN  40565  cdlemk55u1  40568  cdlemk39u1  40570  cdlemk56  40574  cdlemm10N  40721  dihord1  40821  dihord2a  40822  dihord2b  40823  dihord10  40826  dihord4  40861  dihord5apre  40865  dihglblem2N  40897  dihjatc1  40914  dihjatc2N  40915  dihjatc3  40916  dihmeetlem15N  40924  dihmeetlem20N  40929  mapdpglem24  41307  hdmap14lem11  41481  hdmap14lem12  41482  flt4lem5  42209  mzpsubst  42310  monotuz  42504  congmul  42530  congsub  42533  ntrclsiso  43639  ntrclskb  43641  ntrclsk3  43642  infleinf  44892  mullimc  45142  mullimcf  45149  0ellimcdiv  45175  limclner  45177  sge0xaddlem2  45960  lincdifsn  47678  itschlc0yqe  48019  itscnhlc0xyqsol  48024  itsclc0xyqsolr  48028  itsclquadeu  48036