Theorem simp12 1203

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 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
2	1	3ad2ant1 1132	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simp112  1302  simp212  1311  simp312  1320  dvdsgcd  16261  coprimeprodsq  16518  pythagtriplem4  16529  pythagtriplem13  16537  pythagtriplem14  16538  pythagtriplem16  16540  pythagtrip  16544  pceu  16556  mremre  17322  lsmpropd  19292  m2cpminvid  21911  decpmatid  21928  mply1topmatcllem  21961  cmpsublem  22559  isfil2  23016  cxple2a  25863  isosctr  25980  brbtwn2  27282  colinearalg  27287  ax5seg  27315  axcontlem4  27344  bayesth  32415  bnj1204  33001  bnj1279  33007  nolesgn2o  33883  nolesgn2ores  33884  nogesgn1o  33885  nogesgn1ores  33886  nolt02o  33907  nogt01o  33908  sslttr  34010  cofsslt  34097  coinitsslt  34098  cofcut2  34100  ofscom  34318  btwndiff  34338  ifscgr  34355  brofs2  34388  brifs2  34389  fscgr  34391  btwnconn1lem1  34398  btwnconn1lem2  34399  btwnconn1lem3  34400  btwnconn1lem4  34401  btwnconn1lem12  34409  seglecgr12im  34421  seglecgr12  34422  ivthALT  34533  islshpcv  37074  lkrshp  37126  lshpsmreu  37130  lshpkrlem5  37135  cvrval3  37434  4noncolr3  37474  4noncolr2  37475  4noncolr1  37476  athgt  37477  3dimlem2  37480  3dimlem3a  37481  3dimlem4a  37484  3dimlem4  37485  3dimlem4OLDN  37486  1cvratex  37494  hlatexch4  37502  ps-2b  37503  3atlem4  37507  llnnleat  37534  2atm  37548  ps-2c  37549  llnmlplnN  37560  lplnnlelln  37564  2atmat  37582  lvoli2  37602  lvolnlelln  37605  4atlem3b  37619  4atlem10  37627  4atlem11a  37628  4atlem11b  37629  4atlem12a  37631  lplncvrlvol2  37636  2lplnja  37640  dalemswapyz  37677  lneq2at  37799  2lnat  37805  cdlema1N  37812  cdlemb  37815  paddasslem15  37855  pmodlem1  37867  llnmod2i2  37884  llnexchb2lem  37889  dalawlem1  37892  dalawlem3  37894  dalawlem4  37895  dalawlem6  37897  dalawlem7  37898  dalawlem9  37900  dalawlem10  37901  dalawlem11  37902  dalawlem12  37903  dalawlem13  37904  dalawlem15  37906  osumcllem5N  37981  osumcllem6N  37982  osumcllem7N  37983  osumcllem9N  37985  osumcllem10N  37986  osumcllem11N  37987  pl42lem1N  38000  lhpmcvr5N  38048  lhp2atne  38055  lhp2at0ne  38057  4atexlempw  38070  4atexlemex6  38095  4atexlem7  38096  ldilco  38137  ltrneq  38170  trlval2  38184  trlnidat  38194  cdlemd7  38225  cdleme7aa  38263  cdleme7c  38266  cdleme7d  38267  cdleme7e  38268  cdleme7ga  38269  cdleme7  38270  cdleme11c  38282  cdleme11e  38284  cdleme11l  38290  cdleme11  38291  cdleme14  38294  cdleme15a  38295  cdleme15c  38297  cdleme16b  38300  cdleme16c  38301  cdleme16d  38302  cdleme16e  38303  cdleme16f  38304  cdleme0nex  38311  cdleme18d  38316  cdleme19b  38325  cdleme19d  38327  cdleme19e  38328  cdleme20f  38335  cdleme20k  38340  cdleme20l1  38341  cdleme20l2  38342  cdleme20l  38343  cdleme20m  38344  cdleme21a  38346  cdleme21b  38347  cdleme21ct  38350  cdleme21d  38351  cdleme21e  38352  cdleme21f  38353  cdleme21h  38355  cdleme21i  38356  cdleme22eALTN  38366  cdleme22f2  38368  cdleme22g  38369  cdleme24  38373  cdleme25a  38374  cdleme25c  38376  cdleme25dN  38377  cdleme26e  38380  cdleme26ee  38381  cdleme26eALTN  38382  cdleme27N  38390  cdleme28a  38391  cdleme28b  38392  cdleme28  38394  cdlemefr32sn2aw  38425  cdlemefs32sn1aw  38435  cdleme43fsv1snlem  38441  cdleme41sn3a  38454  cdleme32c  38464  cdleme32e  38466  cdleme32le  38468  cdleme35a  38469  cdleme35b  38471  cdleme35c  38472  cdleme35e  38474  cdleme35f  38475  cdleme36a  38481  cdleme36m  38482  cdleme39a  38486  cdleme40m  38488  cdleme40n  38489  cdleme43bN  38511  cdleme43dN  38513  cdleme46f2g2  38514  cdleme46f2g1  38515  cdleme17d2  38516  cdleme4gfv  38528  cdlemeg49le  38532  cdlemeg46c  38534  cdlemeg46fvaw  38537  cdlemeg46nlpq  38538  cdlemeg46gfre  38553  cdleme50trn2  38572  cdleme  38581  cdlemg2idN  38617  cdlemg7fvbwN  38628  cdlemg10bALTN  38657  cdlemg10a  38661  cdlemg12d  38667  cdlemg12g  38670  cdlemg12  38671  cdlemg13a  38672  cdlemg13  38673  cdlemg17b  38683  cdlemg17dN  38684  cdlemg17dALTN  38685  cdlemg17e  38686  cdlemg17f  38687  cdlemg17i  38690  cdlemg17pq  38693  cdlemg17bq  38694  cdlemg17iqN  38695  cdlemg18d  38702  cdlemg18  38703  cdlemg19a  38704  cdlemg19  38705  cdlemg21  38707  cdlemg27a  38713  cdlemg28a  38714  cdlemg31b0N  38715  cdlemg27b  38717  cdlemg31c  38720  cdlemg33b0  38722  cdlemg33c0  38723  cdlemg28  38725  cdlemg33a  38727  cdlemg33  38732  cdlemg36  38735  ltrnco  38740  cdlemg44  38754  cdlemg47  38757  tendococl  38793  tendoplcl  38802  cdlemh1  38836  cdlemh2  38837  cdlemh  38838  cdlemi  38841  tendocan  38845  cdlemk5  38857  cdlemk6  38858  cdlemk7  38869  cdlemk11  38870  cdlemk12  38871  cdlemkole  38874  cdlemk14  38875  cdlemk15  38876  cdlemk16a  38877  cdlemk16  38878  cdlemk18  38889  cdlemk19  38890  cdlemk7u  38891  cdlemk11u  38892  cdlemk12u  38893  cdlemk21N  38894  cdlemk20  38895  cdlemkoatnle-2N  38896  cdlemk13-2N  38897  cdlemkole-2N  38898  cdlemk14-2N  38899  cdlemk15-2N  38900  cdlemk16-2N  38901  cdlemk17-2N  38902  cdlemk18-2N  38907  cdlemk19-2N  38908  cdlemk7u-2N  38909  cdlemk11u-2N  38910  cdlemk12u-2N  38911  cdlemk21-2N  38912  cdlemk20-2N  38913  cdlemk22  38914  cdlemk27-3  38928  cdlemk33N  38930  cdlemk11ta  38950  cdlemkid3N  38954  cdlemk11tc  38966  cdlemk11t  38967  cdlemk45  38968  cdlemk46  38969  cdlemk47  38970  cdlemk48  38971  cdlemk49  38972  cdlemk50  38973  cdlemk51  38974  cdlemk52  38975  cdlemk53a  38976  cdlemk55b  38981  cdlemkyyN  38983  cdlemk55u1  38986  cdlemk39u1  38988  cdlemk56  38992  cdlemm10N  39139  dihord1  39239  dihord2a  39240  dihord2b  39241  dihord10  39244  dihord4  39279  dihord5apre  39283  dihglblem2N  39315  dihjatc1  39332  dihjatc2N  39333  dihjatc3  39334  dihmeetlem15N  39342  dihmeetlem20N  39347  mapdpglem24  39725  hdmap14lem11  39899  hdmap14lem12  39900  flt4lem5  40494  mzpsubst  40577  monotuz  40770  congmul  40796  congsub  40799  ntrclsiso  41684  ntrclskb  41686  ntrclsk3  41687  infleinf  42918  mullimc  43164  mullimcf  43171  0ellimcdiv  43197  limclner  43199  sge0xaddlem2  43979  lincdifsn  45776  itschlc0yqe  46117  itscnhlc0xyqsol  46122  itsclc0xyqsolr  46126  itsclquadeu  46134