Theorem simp12 1202

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 1087

This theorem is referenced by:  simp112  1301  simp212  1310  simp312  1319  dvdsgcd  16492  coprimeprodsq  16747  pythagtriplem4  16758  pythagtriplem13  16766  pythagtriplem14  16767  pythagtriplem16  16769  pythagtrip  16773  pceu  16785  mremre  17554  lsmpropd  19588  m2cpminvid  22477  decpmatid  22494  mply1topmatcllem  22527  cmpsublem  23125  isfil2  23582  cxple2a  26441  isosctr  26560  nolesgn2o  27408  nolesgn2ores  27409  nogesgn1o  27410  nogesgn1ores  27411  nolt02o  27432  nogt01o  27433  sslttr  27543  cofsslt  27641  coinitsslt  27642  cofcut2  27645  brbtwn2  28428  colinearalg  28433  ax5seg  28461  axcontlem4  28490  bayesth  33734  bnj1204  34319  bnj1279  34325  ofscom  35281  btwndiff  35301  ifscgr  35318  brofs2  35351  brifs2  35352  fscgr  35354  btwnconn1lem1  35361  btwnconn1lem2  35362  btwnconn1lem3  35363  btwnconn1lem4  35364  btwnconn1lem12  35372  seglecgr12im  35384  seglecgr12  35385  ivthALT  35525  islshpcv  38228  lkrshp  38280  lshpsmreu  38284  lshpkrlem5  38289  cvrval3  38589  4noncolr3  38629  4noncolr2  38630  4noncolr1  38631  athgt  38632  3dimlem2  38635  3dimlem3a  38636  3dimlem4a  38639  3dimlem4  38640  3dimlem4OLDN  38641  1cvratex  38649  hlatexch4  38657  ps-2b  38658  3atlem4  38662  llnnleat  38689  2atm  38703  ps-2c  38704  llnmlplnN  38715  lplnnlelln  38719  2atmat  38737  lvoli2  38757  lvolnlelln  38760  4atlem3b  38774  4atlem10  38782  4atlem11a  38783  4atlem11b  38784  4atlem12a  38786  lplncvrlvol2  38791  2lplnja  38795  dalemswapyz  38832  lneq2at  38954  2lnat  38960  cdlema1N  38967  cdlemb  38970  paddasslem15  39010  pmodlem1  39022  llnmod2i2  39039  llnexchb2lem  39044  dalawlem1  39047  dalawlem3  39049  dalawlem4  39050  dalawlem6  39052  dalawlem7  39053  dalawlem9  39055  dalawlem10  39056  dalawlem11  39057  dalawlem12  39058  dalawlem13  39059  dalawlem15  39061  osumcllem5N  39136  osumcllem6N  39137  osumcllem7N  39138  osumcllem9N  39140  osumcllem10N  39141  osumcllem11N  39142  pl42lem1N  39155  lhpmcvr5N  39203  lhp2atne  39210  lhp2at0ne  39212  4atexlempw  39225  4atexlemex6  39250  4atexlem7  39251  ldilco  39292  ltrneq  39325  trlval2  39339  trlnidat  39349  cdlemd7  39380  cdleme7aa  39418  cdleme7c  39421  cdleme7d  39422  cdleme7e  39423  cdleme7ga  39424  cdleme7  39425  cdleme11c  39437  cdleme11e  39439  cdleme11l  39445  cdleme11  39446  cdleme14  39449  cdleme15a  39450  cdleme15c  39452  cdleme16b  39455  cdleme16c  39456  cdleme16d  39457  cdleme16e  39458  cdleme16f  39459  cdleme0nex  39466  cdleme18d  39471  cdleme19b  39480  cdleme19d  39482  cdleme19e  39483  cdleme20f  39490  cdleme20k  39495  cdleme20l1  39496  cdleme20l2  39497  cdleme20l  39498  cdleme20m  39499  cdleme21a  39501  cdleme21b  39502  cdleme21ct  39505  cdleme21d  39506  cdleme21e  39507  cdleme21f  39508  cdleme21h  39510  cdleme21i  39511  cdleme22eALTN  39521  cdleme22f2  39523  cdleme22g  39524  cdleme24  39528  cdleme25a  39529  cdleme25c  39531  cdleme25dN  39532  cdleme26e  39535  cdleme26ee  39536  cdleme26eALTN  39537  cdleme27N  39545  cdleme28a  39546  cdleme28b  39547  cdleme28  39549  cdlemefr32sn2aw  39580  cdlemefs32sn1aw  39590  cdleme43fsv1snlem  39596  cdleme41sn3a  39609  cdleme32c  39619  cdleme32e  39621  cdleme32le  39623  cdleme35a  39624  cdleme35b  39626  cdleme35c  39627  cdleme35e  39629  cdleme35f  39630  cdleme36a  39636  cdleme36m  39637  cdleme39a  39641  cdleme40m  39643  cdleme40n  39644  cdleme43bN  39666  cdleme43dN  39668  cdleme46f2g2  39669  cdleme46f2g1  39670  cdleme17d2  39671  cdleme4gfv  39683  cdlemeg49le  39687  cdlemeg46c  39689  cdlemeg46fvaw  39692  cdlemeg46nlpq  39693  cdlemeg46gfre  39708  cdleme50trn2  39727  cdleme  39736  cdlemg2idN  39772  cdlemg7fvbwN  39783  cdlemg10bALTN  39812  cdlemg10a  39816  cdlemg12d  39822  cdlemg12g  39825  cdlemg12  39826  cdlemg13a  39827  cdlemg13  39828  cdlemg17b  39838  cdlemg17dN  39839  cdlemg17dALTN  39840  cdlemg17e  39841  cdlemg17f  39842  cdlemg17i  39845  cdlemg17pq  39848  cdlemg17bq  39849  cdlemg17iqN  39850  cdlemg18d  39857  cdlemg18  39858  cdlemg19a  39859  cdlemg19  39860  cdlemg21  39862  cdlemg27a  39868  cdlemg28a  39869  cdlemg31b0N  39870  cdlemg27b  39872  cdlemg31c  39875  cdlemg33b0  39877  cdlemg33c0  39878  cdlemg28  39880  cdlemg33a  39882  cdlemg33  39887  cdlemg36  39890  ltrnco  39895  cdlemg44  39909  cdlemg47  39912  tendococl  39948  tendoplcl  39957  cdlemh1  39991  cdlemh2  39992  cdlemh  39993  cdlemi  39996  tendocan  40000  cdlemk5  40012  cdlemk6  40013  cdlemk7  40024  cdlemk11  40025  cdlemk12  40026  cdlemkole  40029  cdlemk14  40030  cdlemk15  40031  cdlemk16a  40032  cdlemk16  40033  cdlemk18  40044  cdlemk19  40045  cdlemk7u  40046  cdlemk11u  40047  cdlemk12u  40048  cdlemk21N  40049  cdlemk20  40050  cdlemkoatnle-2N  40051  cdlemk13-2N  40052  cdlemkole-2N  40053  cdlemk14-2N  40054  cdlemk15-2N  40055  cdlemk16-2N  40056  cdlemk17-2N  40057  cdlemk18-2N  40062  cdlemk19-2N  40063  cdlemk7u-2N  40064  cdlemk11u-2N  40065  cdlemk12u-2N  40066  cdlemk21-2N  40067  cdlemk20-2N  40068  cdlemk22  40069  cdlemk27-3  40083  cdlemk33N  40085  cdlemk11ta  40105  cdlemkid3N  40109  cdlemk11tc  40121  cdlemk11t  40122  cdlemk45  40123  cdlemk46  40124  cdlemk47  40125  cdlemk48  40126  cdlemk49  40127  cdlemk50  40128  cdlemk51  40129  cdlemk52  40130  cdlemk53a  40131  cdlemk55b  40136  cdlemkyyN  40138  cdlemk55u1  40141  cdlemk39u1  40143  cdlemk56  40147  cdlemm10N  40294  dihord1  40394  dihord2a  40395  dihord2b  40396  dihord10  40399  dihord4  40434  dihord5apre  40438  dihglblem2N  40470  dihjatc1  40487  dihjatc2N  40488  dihjatc3  40489  dihmeetlem15N  40497  dihmeetlem20N  40502  mapdpglem24  40880  hdmap14lem11  41054  hdmap14lem12  41055  flt4lem5  41696  mzpsubst  41790  monotuz  41984  congmul  42010  congsub  42013  ntrclsiso  43122  ntrclskb  43124  ntrclsk3  43125  infleinf  44382  mullimc  44632  mullimcf  44639  0ellimcdiv  44665  limclner  44667  sge0xaddlem2  45450  lincdifsn  47194  itschlc0yqe  47535  itscnhlc0xyqsol  47540  itsclc0xyqsolr  47544  itsclquadeu  47552