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  16457  coprimeprodsq  16722  pythagtriplem4  16733  pythagtriplem13  16741  pythagtriplem14  16742  pythagtriplem16  16744  pythagtrip  16748  pceu  16760  mremre  17508  lsmpropd  19591  m2cpminvid  22669  decpmatid  22686  mply1topmatcllem  22719  cmpsublem  23315  isfil2  23772  cxple2a  26636  isosctr  26759  nolesgn2o  27611  nolesgn2ores  27612  nogesgn1o  27613  nogesgn1ores  27614  nolt02o  27635  nogt01o  27636  sslttr  27749  cofsslt  27863  coinitsslt  27864  cofcut2  27867  onsfi  28284  brbtwn2  28885  colinearalg  28890  ax5seg  28918  axcontlem4  28947  bayesth  34473  bnj1204  35045  bnj1279  35051  ofscom  36072  btwndiff  36092  ifscgr  36109  brofs2  36142  brifs2  36143  fscgr  36145  btwnconn1lem1  36152  btwnconn1lem2  36153  btwnconn1lem3  36154  btwnconn1lem4  36155  btwnconn1lem12  36163  seglecgr12im  36175  seglecgr12  36176  ivthALT  36400  islshpcv  39172  lkrshp  39224  lshpsmreu  39228  lshpkrlem5  39233  cvrval3  39532  4noncolr3  39572  4noncolr2  39573  4noncolr1  39574  athgt  39575  3dimlem2  39578  3dimlem3a  39579  3dimlem4a  39582  3dimlem4  39583  3dimlem4OLDN  39584  1cvratex  39592  hlatexch4  39600  ps-2b  39601  3atlem4  39605  llnnleat  39632  2atm  39646  ps-2c  39647  llnmlplnN  39658  lplnnlelln  39662  2atmat  39680  lvoli2  39700  lvolnlelln  39703  4atlem3b  39717  4atlem10  39725  4atlem11a  39726  4atlem11b  39727  4atlem12a  39729  lplncvrlvol2  39734  2lplnja  39738  dalemswapyz  39775  lneq2at  39897  2lnat  39903  cdlema1N  39910  cdlemb  39913  paddasslem15  39953  pmodlem1  39965  llnmod2i2  39982  llnexchb2lem  39987  dalawlem1  39990  dalawlem3  39992  dalawlem4  39993  dalawlem6  39995  dalawlem7  39996  dalawlem9  39998  dalawlem10  39999  dalawlem11  40000  dalawlem12  40001  dalawlem13  40002  dalawlem15  40004  osumcllem5N  40079  osumcllem6N  40080  osumcllem7N  40081  osumcllem9N  40083  osumcllem10N  40084  osumcllem11N  40085  pl42lem1N  40098  lhpmcvr5N  40146  lhp2atne  40153  lhp2at0ne  40155  4atexlempw  40168  4atexlemex6  40193  4atexlem7  40194  ldilco  40235  ltrneq  40268  trlval2  40282  trlnidat  40292  cdlemd7  40323  cdleme7aa  40361  cdleme7c  40364  cdleme7d  40365  cdleme7e  40366  cdleme7ga  40367  cdleme7  40368  cdleme11c  40380  cdleme11e  40382  cdleme11l  40388  cdleme11  40389  cdleme14  40392  cdleme15a  40393  cdleme15c  40395  cdleme16b  40398  cdleme16c  40399  cdleme16d  40400  cdleme16e  40401  cdleme16f  40402  cdleme0nex  40409  cdleme18d  40414  cdleme19b  40423  cdleme19d  40425  cdleme19e  40426  cdleme20f  40433  cdleme20k  40438  cdleme20l1  40439  cdleme20l2  40440  cdleme20l  40441  cdleme20m  40442  cdleme21a  40444  cdleme21b  40445  cdleme21ct  40448  cdleme21d  40449  cdleme21e  40450  cdleme21f  40451  cdleme21h  40453  cdleme21i  40454  cdleme22eALTN  40464  cdleme22f2  40466  cdleme22g  40467  cdleme24  40471  cdleme25a  40472  cdleme25c  40474  cdleme25dN  40475  cdleme26e  40478  cdleme26ee  40479  cdleme26eALTN  40480  cdleme27N  40488  cdleme28a  40489  cdleme28b  40490  cdleme28  40492  cdlemefr32sn2aw  40523  cdlemefs32sn1aw  40533  cdleme43fsv1snlem  40539  cdleme41sn3a  40552  cdleme32c  40562  cdleme32e  40564  cdleme32le  40566  cdleme35a  40567  cdleme35b  40569  cdleme35c  40570  cdleme35e  40572  cdleme35f  40573  cdleme36a  40579  cdleme36m  40580  cdleme39a  40584  cdleme40m  40586  cdleme40n  40587  cdleme43bN  40609  cdleme43dN  40611  cdleme46f2g2  40612  cdleme46f2g1  40613  cdleme17d2  40614  cdleme4gfv  40626  cdlemeg49le  40630  cdlemeg46c  40632  cdlemeg46fvaw  40635  cdlemeg46nlpq  40636  cdlemeg46gfre  40651  cdleme50trn2  40670  cdleme  40679  cdlemg2idN  40715  cdlemg7fvbwN  40726  cdlemg10bALTN  40755  cdlemg10a  40759  cdlemg12d  40765  cdlemg12g  40768  cdlemg12  40769  cdlemg13a  40770  cdlemg13  40771  cdlemg17b  40781  cdlemg17dN  40782  cdlemg17dALTN  40783  cdlemg17e  40784  cdlemg17f  40785  cdlemg17i  40788  cdlemg17pq  40791  cdlemg17bq  40792  cdlemg17iqN  40793  cdlemg18d  40800  cdlemg18  40801  cdlemg19a  40802  cdlemg19  40803  cdlemg21  40805  cdlemg27a  40811  cdlemg28a  40812  cdlemg31b0N  40813  cdlemg27b  40815  cdlemg31c  40818  cdlemg33b0  40820  cdlemg33c0  40821  cdlemg28  40823  cdlemg33a  40825  cdlemg33  40830  cdlemg36  40833  ltrnco  40838  cdlemg44  40852  cdlemg47  40855  tendococl  40891  tendoplcl  40900  cdlemh1  40934  cdlemh2  40935  cdlemh  40936  cdlemi  40939  tendocan  40943  cdlemk5  40955  cdlemk6  40956  cdlemk7  40967  cdlemk11  40968  cdlemk12  40969  cdlemkole  40972  cdlemk14  40973  cdlemk15  40974  cdlemk16a  40975  cdlemk16  40976  cdlemk18  40987  cdlemk19  40988  cdlemk7u  40989  cdlemk11u  40990  cdlemk12u  40991  cdlemk21N  40992  cdlemk20  40993  cdlemkoatnle-2N  40994  cdlemk13-2N  40995  cdlemkole-2N  40996  cdlemk14-2N  40997  cdlemk15-2N  40998  cdlemk16-2N  40999  cdlemk17-2N  41000  cdlemk18-2N  41005  cdlemk19-2N  41006  cdlemk7u-2N  41007  cdlemk11u-2N  41008  cdlemk12u-2N  41009  cdlemk21-2N  41010  cdlemk20-2N  41011  cdlemk22  41012  cdlemk27-3  41026  cdlemk33N  41028  cdlemk11ta  41048  cdlemkid3N  41052  cdlemk11tc  41064  cdlemk11t  41065  cdlemk45  41066  cdlemk46  41067  cdlemk47  41068  cdlemk48  41069  cdlemk49  41070  cdlemk50  41071  cdlemk51  41072  cdlemk52  41073  cdlemk53a  41074  cdlemk55b  41079  cdlemkyyN  41081  cdlemk55u1  41084  cdlemk39u1  41086  cdlemk56  41090  cdlemm10N  41237  dihord1  41337  dihord2a  41338  dihord2b  41339  dihord10  41342  dihord4  41377  dihord5apre  41381  dihglblem2N  41413  dihjatc1  41430  dihjatc2N  41431  dihjatc3  41432  dihmeetlem15N  41440  dihmeetlem20N  41445  mapdpglem24  41823  hdmap14lem11  41997  hdmap14lem12  41998  flt4lem5  42768  mzpsubst  42865  monotuz  43058  congmul  43084  congsub  43087  ntrclsiso  44184  ntrclskb  44186  ntrclsk3  44187  infleinf  45494  mullimc  45740  mullimcf  45747  0ellimcdiv  45771  limclner  45773  sge0xaddlem2  46556  isubgr3stgrlem3  48092  lincdifsn  48549  itschlc0yqe  48885  itscnhlc0xyqsol  48890  itsclc0xyqsolr  48894  itsclquadeu  48902