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  16627  coprimeprodsq  16893  pythagtriplem4  16904  pythagtriplem13  16912  pythagtriplem14  16913  pythagtriplem16  16915  pythagtrip  16919  pceu  16931  mremre  17681  lsmpropd  19778  m2cpminvid  22947  decpmatid  22964  mply1topmatcllem  22997  cmpsublem  23593  isfil2  24050  cxple2a  26901  isosctr  27023  nolesgn2o  27872  nolesgn2ores  27873  nogesgn1o  27874  nogesgn1ores  27875  nolt02o  27896  nogt01o  27897  sltstr  28017  cofslts  28148  coinitslts  28149  cofcut2  28152  onsfi  28586  brbtwn2  29292  colinearalg  29297  ax5seg  29325  axcontlem4  29354  bayesth  34861  bnj1204  35432  bnj1279  35438  ofscom  36520  btwndiff  36540  ifscgr  36557  brofs2  36590  brifs2  36591  fscgr  36593  btwnconn1lem1  36600  btwnconn1lem2  36601  btwnconn1lem3  36602  btwnconn1lem4  36603  btwnconn1lem12  36611  seglecgr12im  36623  seglecgr12  36624  ivthALT  36887  islshpcv  39868  lkrshp  39920  lshpsmreu  39924  lshpkrlem5  39929  cvrval3  40228  4noncolr3  40268  4noncolr2  40269  4noncolr1  40270  athgt  40271  3dimlem2  40274  3dimlem3a  40275  3dimlem4a  40278  3dimlem4  40279  3dimlem4OLDN  40280  1cvratex  40288  hlatexch4  40296  ps-2b  40297  3atlem4  40301  llnnleat  40328  2atm  40342  ps-2c  40343  llnmlplnN  40354  lplnnlelln  40358  2atmat  40376  lvoli2  40396  lvolnlelln  40399  4atlem3b  40413  4atlem10  40421  4atlem11a  40422  4atlem11b  40423  4atlem12a  40425  lplncvrlvol2  40430  2lplnja  40434  dalemswapyz  40471  lneq2at  40593  2lnat  40599  cdlema1N  40606  cdlemb  40609  paddasslem15  40649  pmodlem1  40661  llnmod2i2  40678  llnexchb2lem  40683  dalawlem1  40686  dalawlem3  40688  dalawlem4  40689  dalawlem6  40691  dalawlem7  40692  dalawlem9  40694  dalawlem10  40695  dalawlem11  40696  dalawlem12  40697  dalawlem13  40698  dalawlem15  40700  osumcllem5N  40775  osumcllem6N  40776  osumcllem7N  40777  osumcllem9N  40779  osumcllem10N  40780  osumcllem11N  40781  pl42lem1N  40794  lhpmcvr5N  40842  lhp2atne  40849  lhp2at0ne  40851  4atexlempw  40864  4atexlemex6  40889  4atexlem7  40890  ldilco  40931  ltrneq  40964  trlval2  40978  trlnidat  40988  cdlemd7  41019  cdleme7aa  41057  cdleme7c  41060  cdleme7d  41061  cdleme7e  41062  cdleme7ga  41063  cdleme7  41064  cdleme11c  41076  cdleme11e  41078  cdleme11l  41084  cdleme11  41085  cdleme14  41088  cdleme15a  41089  cdleme15c  41091  cdleme16b  41094  cdleme16c  41095  cdleme16d  41096  cdleme16e  41097  cdleme16f  41098  cdleme0nex  41105  cdleme18d  41110  cdleme19b  41119  cdleme19d  41121  cdleme19e  41122  cdleme20f  41129  cdleme20k  41134  cdleme20l1  41135  cdleme20l2  41136  cdleme20l  41137  cdleme20m  41138  cdleme21a  41140  cdleme21b  41141  cdleme21ct  41144  cdleme21d  41145  cdleme21e  41146  cdleme21f  41147  cdleme21h  41149  cdleme21i  41150  cdleme22eALTN  41160  cdleme22f2  41162  cdleme22g  41163  cdleme24  41167  cdleme25a  41168  cdleme25c  41170  cdleme25dN  41171  cdleme26e  41174  cdleme26ee  41175  cdleme26eALTN  41176  cdleme27N  41184  cdleme28a  41185  cdleme28b  41186  cdleme28  41188  cdlemefr32sn2aw  41219  cdlemefs32sn1aw  41229  cdleme43fsv1snlem  41235  cdleme41sn3a  41248  cdleme32c  41258  cdleme32e  41260  cdleme32le  41262  cdleme35a  41263  cdleme35b  41265  cdleme35c  41266  cdleme35e  41268  cdleme35f  41269  cdleme36a  41275  cdleme36m  41276  cdleme39a  41280  cdleme40m  41282  cdleme40n  41283  cdleme43bN  41305  cdleme43dN  41307  cdleme46f2g2  41308  cdleme46f2g1  41309  cdleme17d2  41310  cdleme4gfv  41322  cdlemeg49le  41326  cdlemeg46c  41328  cdlemeg46fvaw  41331  cdlemeg46nlpq  41332  cdlemeg46gfre  41347  cdleme50trn2  41366  cdleme  41375  cdlemg2idN  41411  cdlemg7fvbwN  41422  cdlemg10bALTN  41451  cdlemg10a  41455  cdlemg12d  41461  cdlemg12g  41464  cdlemg12  41465  cdlemg13a  41466  cdlemg13  41467  cdlemg17b  41477  cdlemg17dN  41478  cdlemg17dALTN  41479  cdlemg17e  41480  cdlemg17f  41481  cdlemg17i  41484  cdlemg17pq  41487  cdlemg17bq  41488  cdlemg17iqN  41489  cdlemg18d  41496  cdlemg18  41497  cdlemg19a  41498  cdlemg19  41499  cdlemg21  41501  cdlemg27a  41507  cdlemg28a  41508  cdlemg31b0N  41509  cdlemg27b  41511  cdlemg31c  41514  cdlemg33b0  41516  cdlemg33c0  41517  cdlemg28  41519  cdlemg33a  41521  cdlemg33  41526  cdlemg36  41529  ltrnco  41534  cdlemg44  41548  cdlemg47  41551  tendococl  41587  tendoplcl  41596  cdlemh1  41630  cdlemh2  41631  cdlemh  41632  cdlemi  41635  tendocan  41639  cdlemk5  41651  cdlemk6  41652  cdlemk7  41663  cdlemk11  41664  cdlemk12  41665  cdlemkole  41668  cdlemk14  41669  cdlemk15  41670  cdlemk16a  41671  cdlemk16  41672  cdlemk18  41683  cdlemk19  41684  cdlemk7u  41685  cdlemk11u  41686  cdlemk12u  41687  cdlemk21N  41688  cdlemk20  41689  cdlemkoatnle-2N  41690  cdlemk13-2N  41691  cdlemkole-2N  41692  cdlemk14-2N  41693  cdlemk15-2N  41694  cdlemk16-2N  41695  cdlemk17-2N  41696  cdlemk18-2N  41701  cdlemk19-2N  41702  cdlemk7u-2N  41703  cdlemk11u-2N  41704  cdlemk12u-2N  41705  cdlemk21-2N  41706  cdlemk20-2N  41707  cdlemk22  41708  cdlemk27-3  41722  cdlemk33N  41724  cdlemk11ta  41744  cdlemkid3N  41748  cdlemk11tc  41760  cdlemk11t  41761  cdlemk45  41762  cdlemk46  41763  cdlemk47  41764  cdlemk48  41765  cdlemk49  41766  cdlemk50  41767  cdlemk51  41768  cdlemk52  41769  cdlemk53a  41770  cdlemk55b  41775  cdlemkyyN  41777  cdlemk55u1  41780  cdlemk39u1  41782  cdlemk56  41786  cdlemm10N  41933  dihord1  42033  dihord2a  42034  dihord2b  42035  dihord10  42038  dihord4  42073  dihord5apre  42077  dihglblem2N  42109  dihjatc1  42126  dihjatc2N  42127  dihjatc3  42128  dihmeetlem15N  42136  dihmeetlem20N  42141  mapdpglem24  42519  hdmap14lem11  42693  hdmap14lem12  42694  flt4lem5  43423  mzpsubst  43520  monotuz  43709  congmul  43735  congsub  43738  ntrclsiso  44834  ntrclskb  44836  ntrclsk3  44837  infleinf  46128  mullimc  46373  mullimcf  46380  0ellimcdiv  46404  limclner  46406  sge0xaddlem2  47189  isubgr3stgrlem3  48774  lincdifsn  49245  itschlc0yqe  49581  itscnhlc0xyqsol  49586  itsclc0xyqsolr  49590  itsclquadeu  49598