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  16520  coprimeprodsq  16785  pythagtriplem4  16796  pythagtriplem13  16804  pythagtriplem14  16805  pythagtriplem16  16807  pythagtrip  16811  pceu  16823  mremre  17571  lsmpropd  19613  m2cpminvid  22646  decpmatid  22663  mply1topmatcllem  22696  cmpsublem  23292  isfil2  23749  cxple2a  26614  isosctr  26737  nolesgn2o  27589  nolesgn2ores  27590  nogesgn1o  27591  nogesgn1ores  27592  nolt02o  27613  nogt01o  27614  sslttr  27725  cofsslt  27832  coinitsslt  27833  cofcut2  27836  onsfi  28253  brbtwn2  28838  colinearalg  28843  ax5seg  28871  axcontlem4  28900  bayesth  34436  bnj1204  35008  bnj1279  35014  ofscom  35990  btwndiff  36010  ifscgr  36027  brofs2  36060  brifs2  36061  fscgr  36063  btwnconn1lem1  36070  btwnconn1lem2  36071  btwnconn1lem3  36072  btwnconn1lem4  36073  btwnconn1lem12  36081  seglecgr12im  36093  seglecgr12  36094  ivthALT  36318  islshpcv  39041  lkrshp  39093  lshpsmreu  39097  lshpkrlem5  39102  cvrval3  39402  4noncolr3  39442  4noncolr2  39443  4noncolr1  39444  athgt  39445  3dimlem2  39448  3dimlem3a  39449  3dimlem4a  39452  3dimlem4  39453  3dimlem4OLDN  39454  1cvratex  39462  hlatexch4  39470  ps-2b  39471  3atlem4  39475  llnnleat  39502  2atm  39516  ps-2c  39517  llnmlplnN  39528  lplnnlelln  39532  2atmat  39550  lvoli2  39570  lvolnlelln  39573  4atlem3b  39587  4atlem10  39595  4atlem11a  39596  4atlem11b  39597  4atlem12a  39599  lplncvrlvol2  39604  2lplnja  39608  dalemswapyz  39645  lneq2at  39767  2lnat  39773  cdlema1N  39780  cdlemb  39783  paddasslem15  39823  pmodlem1  39835  llnmod2i2  39852  llnexchb2lem  39857  dalawlem1  39860  dalawlem3  39862  dalawlem4  39863  dalawlem6  39865  dalawlem7  39866  dalawlem9  39868  dalawlem10  39869  dalawlem11  39870  dalawlem12  39871  dalawlem13  39872  dalawlem15  39874  osumcllem5N  39949  osumcllem6N  39950  osumcllem7N  39951  osumcllem9N  39953  osumcllem10N  39954  osumcllem11N  39955  pl42lem1N  39968  lhpmcvr5N  40016  lhp2atne  40023  lhp2at0ne  40025  4atexlempw  40038  4atexlemex6  40063  4atexlem7  40064  ldilco  40105  ltrneq  40138  trlval2  40152  trlnidat  40162  cdlemd7  40193  cdleme7aa  40231  cdleme7c  40234  cdleme7d  40235  cdleme7e  40236  cdleme7ga  40237  cdleme7  40238  cdleme11c  40250  cdleme11e  40252  cdleme11l  40258  cdleme11  40259  cdleme14  40262  cdleme15a  40263  cdleme15c  40265  cdleme16b  40268  cdleme16c  40269  cdleme16d  40270  cdleme16e  40271  cdleme16f  40272  cdleme0nex  40279  cdleme18d  40284  cdleme19b  40293  cdleme19d  40295  cdleme19e  40296  cdleme20f  40303  cdleme20k  40308  cdleme20l1  40309  cdleme20l2  40310  cdleme20l  40311  cdleme20m  40312  cdleme21a  40314  cdleme21b  40315  cdleme21ct  40318  cdleme21d  40319  cdleme21e  40320  cdleme21f  40321  cdleme21h  40323  cdleme21i  40324  cdleme22eALTN  40334  cdleme22f2  40336  cdleme22g  40337  cdleme24  40341  cdleme25a  40342  cdleme25c  40344  cdleme25dN  40345  cdleme26e  40348  cdleme26ee  40349  cdleme26eALTN  40350  cdleme27N  40358  cdleme28a  40359  cdleme28b  40360  cdleme28  40362  cdlemefr32sn2aw  40393  cdlemefs32sn1aw  40403  cdleme43fsv1snlem  40409  cdleme41sn3a  40422  cdleme32c  40432  cdleme32e  40434  cdleme32le  40436  cdleme35a  40437  cdleme35b  40439  cdleme35c  40440  cdleme35e  40442  cdleme35f  40443  cdleme36a  40449  cdleme36m  40450  cdleme39a  40454  cdleme40m  40456  cdleme40n  40457  cdleme43bN  40479  cdleme43dN  40481  cdleme46f2g2  40482  cdleme46f2g1  40483  cdleme17d2  40484  cdleme4gfv  40496  cdlemeg49le  40500  cdlemeg46c  40502  cdlemeg46fvaw  40505  cdlemeg46nlpq  40506  cdlemeg46gfre  40521  cdleme50trn2  40540  cdleme  40549  cdlemg2idN  40585  cdlemg7fvbwN  40596  cdlemg10bALTN  40625  cdlemg10a  40629  cdlemg12d  40635  cdlemg12g  40638  cdlemg12  40639  cdlemg13a  40640  cdlemg13  40641  cdlemg17b  40651  cdlemg17dN  40652  cdlemg17dALTN  40653  cdlemg17e  40654  cdlemg17f  40655  cdlemg17i  40658  cdlemg17pq  40661  cdlemg17bq  40662  cdlemg17iqN  40663  cdlemg18d  40670  cdlemg18  40671  cdlemg19a  40672  cdlemg19  40673  cdlemg21  40675  cdlemg27a  40681  cdlemg28a  40682  cdlemg31b0N  40683  cdlemg27b  40685  cdlemg31c  40688  cdlemg33b0  40690  cdlemg33c0  40691  cdlemg28  40693  cdlemg33a  40695  cdlemg33  40700  cdlemg36  40703  ltrnco  40708  cdlemg44  40722  cdlemg47  40725  tendococl  40761  tendoplcl  40770  cdlemh1  40804  cdlemh2  40805  cdlemh  40806  cdlemi  40809  tendocan  40813  cdlemk5  40825  cdlemk6  40826  cdlemk7  40837  cdlemk11  40838  cdlemk12  40839  cdlemkole  40842  cdlemk14  40843  cdlemk15  40844  cdlemk16a  40845  cdlemk16  40846  cdlemk18  40857  cdlemk19  40858  cdlemk7u  40859  cdlemk11u  40860  cdlemk12u  40861  cdlemk21N  40862  cdlemk20  40863  cdlemkoatnle-2N  40864  cdlemk13-2N  40865  cdlemkole-2N  40866  cdlemk14-2N  40867  cdlemk15-2N  40868  cdlemk16-2N  40869  cdlemk17-2N  40870  cdlemk18-2N  40875  cdlemk19-2N  40876  cdlemk7u-2N  40877  cdlemk11u-2N  40878  cdlemk12u-2N  40879  cdlemk21-2N  40880  cdlemk20-2N  40881  cdlemk22  40882  cdlemk27-3  40896  cdlemk33N  40898  cdlemk11ta  40918  cdlemkid3N  40922  cdlemk11tc  40934  cdlemk11t  40935  cdlemk45  40936  cdlemk46  40937  cdlemk47  40938  cdlemk48  40939  cdlemk49  40940  cdlemk50  40941  cdlemk51  40942  cdlemk52  40943  cdlemk53a  40944  cdlemk55b  40949  cdlemkyyN  40951  cdlemk55u1  40954  cdlemk39u1  40956  cdlemk56  40960  cdlemm10N  41107  dihord1  41207  dihord2a  41208  dihord2b  41209  dihord10  41212  dihord4  41247  dihord5apre  41251  dihglblem2N  41283  dihjatc1  41300  dihjatc2N  41301  dihjatc3  41302  dihmeetlem15N  41310  dihmeetlem20N  41315  mapdpglem24  41693  hdmap14lem11  41867  hdmap14lem12  41868  flt4lem5  42631  mzpsubst  42729  monotuz  42923  congmul  42949  congsub  42952  ntrclsiso  44049  ntrclskb  44051  ntrclsk3  44052  infleinf  45361  mullimc  45607  mullimcf  45614  0ellimcdiv  45640  limclner  45642  sge0xaddlem2  46425  isubgr3stgrlem3  47957  lincdifsn  48403  itschlc0yqe  48739  itscnhlc0xyqsol  48744  itsclc0xyqsolr  48748  itsclquadeu  48756