Theorem simp12 1254

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

Syntax hints:   → wi 4   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  simpl12OLD  1325  simpr12OLD  1343  simp112  1395  simp212  1404  simp312  1413  dvdsgcd  15483  coprimeprodsq  15733  pythagtriplem4  15744  pythagtriplem13  15752  pythagtriplem14  15753  pythagtriplem16  15755  pythagtrip  15759  pceu  15771  mremre  16472  lsmpropd  18294  m2cpminvid  20775  decpmatid  20792  mply1topmatcllem  20825  cmpsublem  21420  isfil2  21877  cxple2a  24665  isosctr  24771  brbtwn2  26005  colinearalg  26010  ax5seg  26038  axcontlem4  26067  bayesth  30832  bnj1204  31408  bnj1279  31414  nolesgn2o  32150  nolesgn2ores  32151  nolt02o  32171  ofscom  32440  btwndiff  32460  ifscgr  32477  brofs2  32510  brifs2  32511  fscgr  32513  btwnconn1lem1  32520  btwnconn1lem2  32521  btwnconn1lem3  32522  btwnconn1lem4  32523  btwnconn1lem12  32531  seglecgr12im  32543  seglecgr12  32544  ivthALT  32656  islshpcv  34835  lkrshp  34887  lshpsmreu  34891  lshpkrlem5  34896  cvrval3  35195  4noncolr3  35235  4noncolr2  35236  4noncolr1  35237  athgt  35238  3dimlem2  35241  3dimlem3a  35242  3dimlem4a  35245  3dimlem4  35246  3dimlem4OLDN  35247  1cvratex  35255  hlatexch4  35263  ps-2b  35264  3atlem4  35268  llnnleat  35295  2atm  35309  ps-2c  35310  llnmlplnN  35321  lplnnlelln  35325  2atmat  35343  lvoli2  35363  lvolnlelln  35366  4atlem3b  35380  4atlem10  35388  4atlem11a  35389  4atlem11b  35390  4atlem12a  35392  lplncvrlvol2  35397  2lplnja  35401  dalemswapyz  35438  lneq2at  35560  2lnat  35566  cdlema1N  35573  cdlemb  35576  paddasslem15  35616  pmodlem1  35628  llnmod2i2  35645  llnexchb2lem  35650  dalawlem1  35653  dalawlem3  35655  dalawlem4  35656  dalawlem6  35658  dalawlem7  35659  dalawlem9  35661  dalawlem10  35662  dalawlem11  35663  dalawlem12  35664  dalawlem13  35665  dalawlem15  35667  osumcllem5N  35742  osumcllem6N  35743  osumcllem7N  35744  osumcllem9N  35746  osumcllem10N  35747  osumcllem11N  35748  pl42lem1N  35761  lhpmcvr5N  35809  lhp2atne  35816  lhp2at0ne  35818  4atexlempw  35831  4atexlemex6  35856  4atexlem7  35857  ldilco  35898  ltrneq  35931  trlval2  35945  trlnidat  35955  cdlemd7  35986  cdleme7aa  36024  cdleme7c  36027  cdleme7d  36028  cdleme7e  36029  cdleme7ga  36030  cdleme7  36031  cdleme11c  36043  cdleme11e  36045  cdleme11l  36051  cdleme11  36052  cdleme14  36055  cdleme15a  36056  cdleme15c  36058  cdleme16b  36061  cdleme16c  36062  cdleme16d  36063  cdleme16e  36064  cdleme16f  36065  cdleme0nex  36072  cdleme18d  36077  cdleme19b  36086  cdleme19d  36088  cdleme19e  36089  cdleme20f  36096  cdleme20k  36101  cdleme20l1  36102  cdleme20l2  36103  cdleme20l  36104  cdleme20m  36105  cdleme21a  36107  cdleme21b  36108  cdleme21ct  36111  cdleme21d  36112  cdleme21e  36113  cdleme21f  36114  cdleme21h  36116  cdleme21i  36117  cdleme22eALTN  36127  cdleme22f2  36129  cdleme22g  36130  cdleme24  36134  cdleme25a  36135  cdleme25c  36137  cdleme25dN  36138  cdleme26e  36141  cdleme26ee  36142  cdleme26eALTN  36143  cdleme27N  36151  cdleme28a  36152  cdleme28b  36153  cdleme28  36155  cdlemefr32sn2aw  36186  cdlemefs32sn1aw  36196  cdleme43fsv1snlem  36202  cdleme41sn3a  36215  cdleme32c  36225  cdleme32e  36227  cdleme32le  36229  cdleme35a  36230  cdleme35b  36232  cdleme35c  36233  cdleme35e  36235  cdleme35f  36236  cdleme36a  36242  cdleme36m  36243  cdleme39a  36247  cdleme40m  36249  cdleme40n  36250  cdleme43bN  36272  cdleme43dN  36274  cdleme46f2g2  36275  cdleme46f2g1  36276  cdleme17d2  36277  cdleme4gfv  36289  cdlemeg49le  36293  cdlemeg46c  36295  cdlemeg46fvaw  36298  cdlemeg46nlpq  36299  cdlemeg46gfre  36314  cdleme50trn2  36333  cdleme  36342  cdlemg2idN  36378  cdlemg7fvbwN  36389  cdlemg10bALTN  36418  cdlemg10a  36422  cdlemg12d  36428  cdlemg12g  36431  cdlemg12  36432  cdlemg13a  36433  cdlemg13  36434  cdlemg17b  36444  cdlemg17dN  36445  cdlemg17dALTN  36446  cdlemg17e  36447  cdlemg17f  36448  cdlemg17i  36451  cdlemg17pq  36454  cdlemg17bq  36455  cdlemg17iqN  36456  cdlemg18d  36463  cdlemg18  36464  cdlemg19a  36465  cdlemg19  36466  cdlemg21  36468  cdlemg27a  36474  cdlemg28a  36475  cdlemg31b0N  36476  cdlemg27b  36478  cdlemg31c  36481  cdlemg33b0  36483  cdlemg33c0  36484  cdlemg28  36486  cdlemg33a  36488  cdlemg33  36493  cdlemg36  36496  ltrnco  36501  cdlemg44  36515  cdlemg47  36518  tendococl  36554  tendoplcl  36563  cdlemh1  36597  cdlemh2  36598  cdlemh  36599  cdlemi  36602  tendocan  36606  cdlemk5  36618  cdlemk6  36619  cdlemk7  36630  cdlemk11  36631  cdlemk12  36632  cdlemkole  36635  cdlemk14  36636  cdlemk15  36637  cdlemk16a  36638  cdlemk16  36639  cdlemk18  36650  cdlemk19  36651  cdlemk7u  36652  cdlemk11u  36653  cdlemk12u  36654  cdlemk21N  36655  cdlemk20  36656  cdlemkoatnle-2N  36657  cdlemk13-2N  36658  cdlemkole-2N  36659  cdlemk14-2N  36660  cdlemk15-2N  36661  cdlemk16-2N  36662  cdlemk17-2N  36663  cdlemk18-2N  36668  cdlemk19-2N  36669  cdlemk7u-2N  36670  cdlemk11u-2N  36671  cdlemk12u-2N  36672  cdlemk21-2N  36673  cdlemk20-2N  36674  cdlemk22  36675  cdlemk27-3  36689  cdlemk33N  36691  cdlemk11ta  36711  cdlemkid3N  36715  cdlemk11tc  36727  cdlemk11t  36728  cdlemk45  36729  cdlemk46  36730  cdlemk47  36731  cdlemk48  36732  cdlemk49  36733  cdlemk50  36734  cdlemk51  36735  cdlemk52  36736  cdlemk53a  36737  cdlemk55b  36742  cdlemkyyN  36744  cdlemk55u1  36747  cdlemk39u1  36749  cdlemk56  36753  cdlemm10N  36900  dihord1  37000  dihord2a  37001  dihord2b  37002  dihord10  37005  dihord4  37040  dihord5apre  37044  dihglblem2N  37076  dihjatc1  37093  dihjatc2N  37094  dihjatc3  37095  dihmeetlem15N  37103  dihmeetlem20N  37108  mapdpglem24  37486  hdmap14lem11  37660  hdmap14lem12  37661  mzpsubst  37814  monotuz  38008  congmul  38036  congsub  38039  ntrclsiso  38866  ntrclskb  38868  ntrclsk3  38869  infleinf  40069  mullimc  40329  mullimcf  40336  0ellimcdiv  40362  limclner  40364  sge0xaddlem2  41131  lincdifsn  42782