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  16561  coprimeprodsq  16826  pythagtriplem4  16837  pythagtriplem13  16845  pythagtriplem14  16846  pythagtriplem16  16848  pythagtrip  16852  pceu  16864  mremre  17614  lsmpropd  19656  m2cpminvid  22689  decpmatid  22706  mply1topmatcllem  22739  cmpsublem  23335  isfil2  23792  cxple2a  26658  isosctr  26781  nolesgn2o  27633  nolesgn2ores  27634  nogesgn1o  27635  nogesgn1ores  27636  nolt02o  27657  nogt01o  27658  sslttr  27769  cofsslt  27869  coinitsslt  27870  cofcut2  27873  brbtwn2  28830  colinearalg  28835  ax5seg  28863  axcontlem4  28892  bayesth  34417  bnj1204  34989  bnj1279  34995  ofscom  35971  btwndiff  35991  ifscgr  36008  brofs2  36041  brifs2  36042  fscgr  36044  btwnconn1lem1  36051  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem4  36054  btwnconn1lem12  36062  seglecgr12im  36074  seglecgr12  36075  ivthALT  36299  islshpcv  39017  lkrshp  39069  lshpsmreu  39073  lshpkrlem5  39078  cvrval3  39378  4noncolr3  39418  4noncolr2  39419  4noncolr1  39420  athgt  39421  3dimlem2  39424  3dimlem3a  39425  3dimlem4a  39428  3dimlem4  39429  3dimlem4OLDN  39430  1cvratex  39438  hlatexch4  39446  ps-2b  39447  3atlem4  39451  llnnleat  39478  2atm  39492  ps-2c  39493  llnmlplnN  39504  lplnnlelln  39508  2atmat  39526  lvoli2  39546  lvolnlelln  39549  4atlem3b  39563  4atlem10  39571  4atlem11a  39572  4atlem11b  39573  4atlem12a  39575  lplncvrlvol2  39580  2lplnja  39584  dalemswapyz  39621  lneq2at  39743  2lnat  39749  cdlema1N  39756  cdlemb  39759  paddasslem15  39799  pmodlem1  39811  llnmod2i2  39828  llnexchb2lem  39833  dalawlem1  39836  dalawlem3  39838  dalawlem4  39839  dalawlem6  39841  dalawlem7  39842  dalawlem9  39844  dalawlem10  39845  dalawlem11  39846  dalawlem12  39847  dalawlem13  39848  dalawlem15  39850  osumcllem5N  39925  osumcllem6N  39926  osumcllem7N  39927  osumcllem9N  39929  osumcllem10N  39930  osumcllem11N  39931  pl42lem1N  39944  lhpmcvr5N  39992  lhp2atne  39999  lhp2at0ne  40001  4atexlempw  40014  4atexlemex6  40039  4atexlem7  40040  ldilco  40081  ltrneq  40114  trlval2  40128  trlnidat  40138  cdlemd7  40169  cdleme7aa  40207  cdleme7c  40210  cdleme7d  40211  cdleme7e  40212  cdleme7ga  40213  cdleme7  40214  cdleme11c  40226  cdleme11e  40228  cdleme11l  40234  cdleme11  40235  cdleme14  40238  cdleme15a  40239  cdleme15c  40241  cdleme16b  40244  cdleme16c  40245  cdleme16d  40246  cdleme16e  40247  cdleme16f  40248  cdleme0nex  40255  cdleme18d  40260  cdleme19b  40269  cdleme19d  40271  cdleme19e  40272  cdleme20f  40279  cdleme20k  40284  cdleme20l1  40285  cdleme20l2  40286  cdleme20l  40287  cdleme20m  40288  cdleme21a  40290  cdleme21b  40291  cdleme21ct  40294  cdleme21d  40295  cdleme21e  40296  cdleme21f  40297  cdleme21h  40299  cdleme21i  40300  cdleme22eALTN  40310  cdleme22f2  40312  cdleme22g  40313  cdleme24  40317  cdleme25a  40318  cdleme25c  40320  cdleme25dN  40321  cdleme26e  40324  cdleme26ee  40325  cdleme26eALTN  40326  cdleme27N  40334  cdleme28a  40335  cdleme28b  40336  cdleme28  40338  cdlemefr32sn2aw  40369  cdlemefs32sn1aw  40379  cdleme43fsv1snlem  40385  cdleme41sn3a  40398  cdleme32c  40408  cdleme32e  40410  cdleme32le  40412  cdleme35a  40413  cdleme35b  40415  cdleme35c  40416  cdleme35e  40418  cdleme35f  40419  cdleme36a  40425  cdleme36m  40426  cdleme39a  40430  cdleme40m  40432  cdleme40n  40433  cdleme43bN  40455  cdleme43dN  40457  cdleme46f2g2  40458  cdleme46f2g1  40459  cdleme17d2  40460  cdleme4gfv  40472  cdlemeg49le  40476  cdlemeg46c  40478  cdlemeg46fvaw  40481  cdlemeg46nlpq  40482  cdlemeg46gfre  40497  cdleme50trn2  40516  cdleme  40525  cdlemg2idN  40561  cdlemg7fvbwN  40572  cdlemg10bALTN  40601  cdlemg10a  40605  cdlemg12d  40611  cdlemg12g  40614  cdlemg12  40615  cdlemg13a  40616  cdlemg13  40617  cdlemg17b  40627  cdlemg17dN  40628  cdlemg17dALTN  40629  cdlemg17e  40630  cdlemg17f  40631  cdlemg17i  40634  cdlemg17pq  40637  cdlemg17bq  40638  cdlemg17iqN  40639  cdlemg18d  40646  cdlemg18  40647  cdlemg19a  40648  cdlemg19  40649  cdlemg21  40651  cdlemg27a  40657  cdlemg28a  40658  cdlemg31b0N  40659  cdlemg27b  40661  cdlemg31c  40664  cdlemg33b0  40666  cdlemg33c0  40667  cdlemg28  40669  cdlemg33a  40671  cdlemg33  40676  cdlemg36  40679  ltrnco  40684  cdlemg44  40698  cdlemg47  40701  tendococl  40737  tendoplcl  40746  cdlemh1  40780  cdlemh2  40781  cdlemh  40782  cdlemi  40785  tendocan  40789  cdlemk5  40801  cdlemk6  40802  cdlemk7  40813  cdlemk11  40814  cdlemk12  40815  cdlemkole  40818  cdlemk14  40819  cdlemk15  40820  cdlemk16a  40821  cdlemk16  40822  cdlemk18  40833  cdlemk19  40834  cdlemk7u  40835  cdlemk11u  40836  cdlemk12u  40837  cdlemk21N  40838  cdlemk20  40839  cdlemkoatnle-2N  40840  cdlemk13-2N  40841  cdlemkole-2N  40842  cdlemk14-2N  40843  cdlemk15-2N  40844  cdlemk16-2N  40845  cdlemk17-2N  40846  cdlemk18-2N  40851  cdlemk19-2N  40852  cdlemk7u-2N  40853  cdlemk11u-2N  40854  cdlemk12u-2N  40855  cdlemk21-2N  40856  cdlemk20-2N  40857  cdlemk22  40858  cdlemk27-3  40872  cdlemk33N  40874  cdlemk11ta  40894  cdlemkid3N  40898  cdlemk11tc  40910  cdlemk11t  40911  cdlemk45  40912  cdlemk46  40913  cdlemk47  40914  cdlemk48  40915  cdlemk49  40916  cdlemk50  40917  cdlemk51  40918  cdlemk52  40919  cdlemk53a  40920  cdlemk55b  40925  cdlemkyyN  40927  cdlemk55u1  40930  cdlemk39u1  40932  cdlemk56  40936  cdlemm10N  41083  dihord1  41183  dihord2a  41184  dihord2b  41185  dihord10  41188  dihord4  41223  dihord5apre  41227  dihglblem2N  41259  dihjatc1  41276  dihjatc2N  41277  dihjatc3  41278  dihmeetlem15N  41286  dihmeetlem20N  41291  mapdpglem24  41669  hdmap14lem11  41843  hdmap14lem12  41844  flt4lem5  42620  mzpsubst  42718  monotuz  42912  congmul  42938  congsub  42941  ntrclsiso  44038  ntrclskb  44040  ntrclsk3  44041  infleinf  45347  mullimc  45593  mullimcf  45600  0ellimcdiv  45626  limclner  45628  sge0xaddlem2  46411  isubgr3stgrlem3  47928  lincdifsn  48348  itschlc0yqe  48688  itscnhlc0xyqsol  48693  itsclc0xyqsolr  48697  itsclquadeu  48705