Theorem simp12 1223

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp112  1322  simp212  1331  simp312  1340  dvdsgcd  16640  coprimeprodsq  16906  pythagtriplem4  16917  pythagtriplem13  16925  pythagtriplem14  16926  pythagtriplem16  16928  pythagtrip  16932  pceu  16944  mremre  17694  lsmpropd  19810  m2cpminvid  22984  decpmatid  23001  mply1topmatcllem  23034  cmpsublem  23630  isfil2  24088  cxple2a  26944  isosctr  27066  nolesgn2o  27915  nolesgn2ores  27916  nogesgn1o  27917  nogesgn1ores  27918  nolt02o  27939  nogt01o  27940  sltstr  28060  cofslts  28191  coinitslts  28192  cofcut2  28195  onsfi  28629  brbtwn2  29370  colinearalg  29375  ax5seg  29403  axcontlem4  29432  bayesth  34958  bnj1204  35529  bnj1279  35535  ofscom  36595  btwndiff  36615  ifscgr  36632  brofs2  36665  brifs2  36666  fscgr  36668  btwnconn1lem1  36675  btwnconn1lem2  36676  btwnconn1lem3  36677  btwnconn1lem4  36678  btwnconn1lem12  36686  seglecgr12im  36698  seglecgr12  36699  ivthALT  36962  islshpcv  39934  lkrshp  39986  lshpsmreu  39990  lshpkrlem5  39995  cvrval3  40294  4noncolr3  40334  4noncolr2  40335  4noncolr1  40336  athgt  40337  3dimlem2  40340  3dimlem3a  40341  3dimlem4a  40344  3dimlem4  40345  3dimlem4OLDN  40346  1cvratex  40354  hlatexch4  40362  ps-2b  40363  3atlem4  40367  llnnleat  40394  2atm  40408  ps-2c  40409  llnmlplnN  40420  lplnnlelln  40424  2atmat  40442  lvoli2  40462  lvolnlelln  40465  4atlem3b  40479  4atlem10  40487  4atlem11a  40488  4atlem11b  40489  4atlem12a  40491  lplncvrlvol2  40496  2lplnja  40500  dalemswapyz  40537  lneq2at  40659  2lnat  40665  cdlema1N  40672  cdlemb  40675  paddasslem15  40715  pmodlem1  40727  llnmod2i2  40744  llnexchb2lem  40749  dalawlem1  40752  dalawlem3  40754  dalawlem4  40755  dalawlem6  40757  dalawlem7  40758  dalawlem9  40760  dalawlem10  40761  dalawlem11  40762  dalawlem12  40763  dalawlem13  40764  dalawlem15  40766  osumcllem5N  40841  osumcllem6N  40842  osumcllem7N  40843  osumcllem9N  40845  osumcllem10N  40846  osumcllem11N  40847  pl42lem1N  40860  lhpmcvr5N  40908  lhp2atne  40915  lhp2at0ne  40917  4atexlempw  40930  4atexlemex6  40955  4atexlem7  40956  ldilco  40997  ltrneq  41030  trlval2  41044  trlnidat  41054  cdlemd7  41085  cdleme7aa  41123  cdleme7c  41126  cdleme7d  41127  cdleme7e  41128  cdleme7ga  41129  cdleme7  41130  cdleme11c  41142  cdleme11e  41144  cdleme11l  41150  cdleme11  41151  cdleme14  41154  cdleme15a  41155  cdleme15c  41157  cdleme16b  41160  cdleme16c  41161  cdleme16d  41162  cdleme16e  41163  cdleme16f  41164  cdleme0nex  41171  cdleme18d  41176  cdleme19b  41185  cdleme19d  41187  cdleme19e  41188  cdleme20f  41195  cdleme20k  41200  cdleme20l1  41201  cdleme20l2  41202  cdleme20l  41203  cdleme20m  41204  cdleme21a  41206  cdleme21b  41207  cdleme21ct  41210  cdleme21d  41211  cdleme21e  41212  cdleme21f  41213  cdleme21h  41215  cdleme21i  41216  cdleme22eALTN  41226  cdleme22f2  41228  cdleme22g  41229  cdleme24  41233  cdleme25a  41234  cdleme25c  41236  cdleme25dN  41237  cdleme26e  41240  cdleme26ee  41241  cdleme26eALTN  41242  cdleme27N  41250  cdleme28a  41251  cdleme28b  41252  cdleme28  41254  cdlemefr32sn2aw  41285  cdlemefs32sn1aw  41295  cdleme43fsv1snlem  41301  cdleme41sn3a  41314  cdleme32c  41324  cdleme32e  41326  cdleme32le  41328  cdleme35a  41329  cdleme35b  41331  cdleme35c  41332  cdleme35e  41334  cdleme35f  41335  cdleme36a  41341  cdleme36m  41342  cdleme39a  41346  cdleme40m  41348  cdleme40n  41349  cdleme43bN  41371  cdleme43dN  41373  cdleme46f2g2  41374  cdleme46f2g1  41375  cdleme17d2  41376  cdleme4gfv  41388  cdlemeg49le  41392  cdlemeg46c  41394  cdlemeg46fvaw  41397  cdlemeg46nlpq  41398  cdlemeg46gfre  41413  cdleme50trn2  41432  cdleme  41441  cdlemg2idN  41477  cdlemg7fvbwN  41488  cdlemg10bALTN  41517  cdlemg10a  41521  cdlemg12d  41527  cdlemg12g  41530  cdlemg12  41531  cdlemg13a  41532  cdlemg13  41533  cdlemg17b  41543  cdlemg17dN  41544  cdlemg17dALTN  41545  cdlemg17e  41546  cdlemg17f  41547  cdlemg17i  41550  cdlemg17pq  41553  cdlemg17bq  41554  cdlemg17iqN  41555  cdlemg18d  41562  cdlemg18  41563  cdlemg19a  41564  cdlemg19  41565  cdlemg21  41567  cdlemg27a  41573  cdlemg28a  41574  cdlemg31b0N  41575  cdlemg27b  41577  cdlemg31c  41580  cdlemg33b0  41582  cdlemg33c0  41583  cdlemg28  41585  cdlemg33a  41587  cdlemg33  41592  cdlemg36  41595  ltrnco  41600  cdlemg44  41614  cdlemg47  41617  tendococl  41653  tendoplcl  41662  cdlemh1  41696  cdlemh2  41697  cdlemh  41698  cdlemi  41701  tendocan  41705  cdlemk5  41717  cdlemk6  41718  cdlemk7  41729  cdlemk11  41730  cdlemk12  41731  cdlemkole  41734  cdlemk14  41735  cdlemk15  41736  cdlemk16a  41737  cdlemk16  41738  cdlemk18  41749  cdlemk19  41750  cdlemk7u  41751  cdlemk11u  41752  cdlemk12u  41753  cdlemk21N  41754  cdlemk20  41755  cdlemkoatnle-2N  41756  cdlemk13-2N  41757  cdlemkole-2N  41758  cdlemk14-2N  41759  cdlemk15-2N  41760  cdlemk16-2N  41761  cdlemk17-2N  41762  cdlemk18-2N  41767  cdlemk19-2N  41768  cdlemk7u-2N  41769  cdlemk11u-2N  41770  cdlemk12u-2N  41771  cdlemk21-2N  41772  cdlemk20-2N  41773  cdlemk22  41774  cdlemk27-3  41788  cdlemk33N  41790  cdlemk11ta  41810  cdlemkid3N  41814  cdlemk11tc  41826  cdlemk11t  41827  cdlemk45  41828  cdlemk46  41829  cdlemk47  41830  cdlemk48  41831  cdlemk49  41832  cdlemk50  41833  cdlemk51  41834  cdlemk52  41835  cdlemk53a  41836  cdlemk55b  41841  cdlemkyyN  41843  cdlemk55u1  41846  cdlemk39u1  41848  cdlemk56  41852  cdlemm10N  41999  dihord1  42099  dihord2a  42100  dihord2b  42101  dihord10  42104  dihord4  42139  dihord5apre  42143  dihglblem2N  42175  dihjatc1  42192  dihjatc2N  42193  dihjatc3  42194  dihmeetlem15N  42202  dihmeetlem20N  42207  mapdpglem24  42585  hdmap14lem11  42759  hdmap14lem12  42760  flt4lem5  43504  mzpsubst  43601  monotuz  43790  congmul  43816  congsub  43819  ntrclsiso  44915  ntrclskb  44917  ntrclsk3  44918  infleinf  46209  mullimc  46454  mullimcf  46461  0ellimcdiv  46485  limclner  46487  sge0xaddlem2  47270  isubgr3stgrlem3  48892  lincdifsn  49362  itschlc0yqe  49698  itscnhlc0xyqsol  49703  itsclc0xyqsolr  49707  itsclquadeu  49715