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  16452  coprimeprodsq  16717  pythagtriplem4  16728  pythagtriplem13  16736  pythagtriplem14  16737  pythagtriplem16  16739  pythagtrip  16743  pceu  16755  mremre  17503  lsmpropd  19587  m2cpminvid  22666  decpmatid  22683  mply1topmatcllem  22716  cmpsublem  23312  isfil2  23769  cxple2a  26633  isosctr  26756  nolesgn2o  27608  nolesgn2ores  27609  nogesgn1o  27610  nogesgn1ores  27611  nolt02o  27632  nogt01o  27633  sslttr  27746  cofsslt  27860  coinitsslt  27861  cofcut2  27864  onsfi  28281  brbtwn2  28881  colinearalg  28886  ax5seg  28914  axcontlem4  28943  bayesth  34447  bnj1204  35019  bnj1279  35025  ofscom  36040  btwndiff  36060  ifscgr  36077  brofs2  36110  brifs2  36111  fscgr  36113  btwnconn1lem1  36120  btwnconn1lem2  36121  btwnconn1lem3  36122  btwnconn1lem4  36123  btwnconn1lem12  36131  seglecgr12im  36143  seglecgr12  36144  ivthALT  36368  islshpcv  39091  lkrshp  39143  lshpsmreu  39147  lshpkrlem5  39152  cvrval3  39451  4noncolr3  39491  4noncolr2  39492  4noncolr1  39493  athgt  39494  3dimlem2  39497  3dimlem3a  39498  3dimlem4a  39501  3dimlem4  39502  3dimlem4OLDN  39503  1cvratex  39511  hlatexch4  39519  ps-2b  39520  3atlem4  39524  llnnleat  39551  2atm  39565  ps-2c  39566  llnmlplnN  39577  lplnnlelln  39581  2atmat  39599  lvoli2  39619  lvolnlelln  39622  4atlem3b  39636  4atlem10  39644  4atlem11a  39645  4atlem11b  39646  4atlem12a  39648  lplncvrlvol2  39653  2lplnja  39657  dalemswapyz  39694  lneq2at  39816  2lnat  39822  cdlema1N  39829  cdlemb  39832  paddasslem15  39872  pmodlem1  39884  llnmod2i2  39901  llnexchb2lem  39906  dalawlem1  39909  dalawlem3  39911  dalawlem4  39912  dalawlem6  39914  dalawlem7  39915  dalawlem9  39917  dalawlem10  39918  dalawlem11  39919  dalawlem12  39920  dalawlem13  39921  dalawlem15  39923  osumcllem5N  39998  osumcllem6N  39999  osumcllem7N  40000  osumcllem9N  40002  osumcllem10N  40003  osumcllem11N  40004  pl42lem1N  40017  lhpmcvr5N  40065  lhp2atne  40072  lhp2at0ne  40074  4atexlempw  40087  4atexlemex6  40112  4atexlem7  40113  ldilco  40154  ltrneq  40187  trlval2  40201  trlnidat  40211  cdlemd7  40242  cdleme7aa  40280  cdleme7c  40283  cdleme7d  40284  cdleme7e  40285  cdleme7ga  40286  cdleme7  40287  cdleme11c  40299  cdleme11e  40301  cdleme11l  40307  cdleme11  40308  cdleme14  40311  cdleme15a  40312  cdleme15c  40314  cdleme16b  40317  cdleme16c  40318  cdleme16d  40319  cdleme16e  40320  cdleme16f  40321  cdleme0nex  40328  cdleme18d  40333  cdleme19b  40342  cdleme19d  40344  cdleme19e  40345  cdleme20f  40352  cdleme20k  40357  cdleme20l1  40358  cdleme20l2  40359  cdleme20l  40360  cdleme20m  40361  cdleme21a  40363  cdleme21b  40364  cdleme21ct  40367  cdleme21d  40368  cdleme21e  40369  cdleme21f  40370  cdleme21h  40372  cdleme21i  40373  cdleme22eALTN  40383  cdleme22f2  40385  cdleme22g  40386  cdleme24  40390  cdleme25a  40391  cdleme25c  40393  cdleme25dN  40394  cdleme26e  40397  cdleme26ee  40398  cdleme26eALTN  40399  cdleme27N  40407  cdleme28a  40408  cdleme28b  40409  cdleme28  40411  cdlemefr32sn2aw  40442  cdlemefs32sn1aw  40452  cdleme43fsv1snlem  40458  cdleme41sn3a  40471  cdleme32c  40481  cdleme32e  40483  cdleme32le  40485  cdleme35a  40486  cdleme35b  40488  cdleme35c  40489  cdleme35e  40491  cdleme35f  40492  cdleme36a  40498  cdleme36m  40499  cdleme39a  40503  cdleme40m  40505  cdleme40n  40506  cdleme43bN  40528  cdleme43dN  40530  cdleme46f2g2  40531  cdleme46f2g1  40532  cdleme17d2  40533  cdleme4gfv  40545  cdlemeg49le  40549  cdlemeg46c  40551  cdlemeg46fvaw  40554  cdlemeg46nlpq  40555  cdlemeg46gfre  40570  cdleme50trn2  40589  cdleme  40598  cdlemg2idN  40634  cdlemg7fvbwN  40645  cdlemg10bALTN  40674  cdlemg10a  40678  cdlemg12d  40684  cdlemg12g  40687  cdlemg12  40688  cdlemg13a  40689  cdlemg13  40690  cdlemg17b  40700  cdlemg17dN  40701  cdlemg17dALTN  40702  cdlemg17e  40703  cdlemg17f  40704  cdlemg17i  40707  cdlemg17pq  40710  cdlemg17bq  40711  cdlemg17iqN  40712  cdlemg18d  40719  cdlemg18  40720  cdlemg19a  40721  cdlemg19  40722  cdlemg21  40724  cdlemg27a  40730  cdlemg28a  40731  cdlemg31b0N  40732  cdlemg27b  40734  cdlemg31c  40737  cdlemg33b0  40739  cdlemg33c0  40740  cdlemg28  40742  cdlemg33a  40744  cdlemg33  40749  cdlemg36  40752  ltrnco  40757  cdlemg44  40771  cdlemg47  40774  tendococl  40810  tendoplcl  40819  cdlemh1  40853  cdlemh2  40854  cdlemh  40855  cdlemi  40858  tendocan  40862  cdlemk5  40874  cdlemk6  40875  cdlemk7  40886  cdlemk11  40887  cdlemk12  40888  cdlemkole  40891  cdlemk14  40892  cdlemk15  40893  cdlemk16a  40894  cdlemk16  40895  cdlemk18  40906  cdlemk19  40907  cdlemk7u  40908  cdlemk11u  40909  cdlemk12u  40910  cdlemk21N  40911  cdlemk20  40912  cdlemkoatnle-2N  40913  cdlemk13-2N  40914  cdlemkole-2N  40915  cdlemk14-2N  40916  cdlemk15-2N  40917  cdlemk16-2N  40918  cdlemk17-2N  40919  cdlemk18-2N  40924  cdlemk19-2N  40925  cdlemk7u-2N  40926  cdlemk11u-2N  40927  cdlemk12u-2N  40928  cdlemk21-2N  40929  cdlemk20-2N  40930  cdlemk22  40931  cdlemk27-3  40945  cdlemk33N  40947  cdlemk11ta  40967  cdlemkid3N  40971  cdlemk11tc  40983  cdlemk11t  40984  cdlemk45  40985  cdlemk46  40986  cdlemk47  40987  cdlemk48  40988  cdlemk49  40989  cdlemk50  40990  cdlemk51  40991  cdlemk52  40992  cdlemk53a  40993  cdlemk55b  40998  cdlemkyyN  41000  cdlemk55u1  41003  cdlemk39u1  41005  cdlemk56  41009  cdlemm10N  41156  dihord1  41256  dihord2a  41257  dihord2b  41258  dihord10  41261  dihord4  41296  dihord5apre  41300  dihglblem2N  41332  dihjatc1  41349  dihjatc2N  41350  dihjatc3  41351  dihmeetlem15N  41359  dihmeetlem20N  41364  mapdpglem24  41742  hdmap14lem11  41916  hdmap14lem12  41917  flt4lem5  42682  mzpsubst  42780  monotuz  42973  congmul  42999  congsub  43002  ntrclsiso  44099  ntrclskb  44101  ntrclsk3  44102  infleinf  45409  mullimc  45655  mullimcf  45662  0ellimcdiv  45686  limclner  45688  sge0xaddlem2  46471  isubgr3stgrlem3  47998  lincdifsn  48455  itschlc0yqe  48791  itscnhlc0xyqsol  48796  itsclc0xyqsolr  48800  itsclquadeu  48808