Theorem simp12 1211

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp112  1310  simp212  1319  simp312  1328  dvdsgcd  16511  coprimeprodsq  16777  pythagtriplem4  16788  pythagtriplem13  16796  pythagtriplem14  16797  pythagtriplem16  16799  pythagtrip  16803  pceu  16815  mremre  17564  lsmpropd  19650  m2cpminvid  22743  decpmatid  22760  mply1topmatcllem  22793  cmpsublem  23389  isfil2  23846  cxple2a  26688  isosctr  26810  nolesgn2o  27660  nolesgn2ores  27661  nogesgn1o  27662  nogesgn1ores  27663  nolt02o  27684  nogt01o  27685  sltstr  27804  cofslts  27935  coinitslts  27936  cofcut2  27939  onsfi  28373  brbtwn2  28999  colinearalg  29004  ax5seg  29032  axcontlem4  29061  bayesth  34630  bnj1204  35201  bnj1279  35207  ofscom  36242  btwndiff  36262  ifscgr  36279  brofs2  36312  brifs2  36313  fscgr  36315  btwnconn1lem1  36322  btwnconn1lem2  36323  btwnconn1lem3  36324  btwnconn1lem4  36325  btwnconn1lem12  36333  seglecgr12im  36345  seglecgr12  36346  ivthALT  36570  islshpcv  39552  lkrshp  39604  lshpsmreu  39608  lshpkrlem5  39613  cvrval3  39912  4noncolr3  39952  4noncolr2  39953  4noncolr1  39954  athgt  39955  3dimlem2  39958  3dimlem3a  39959  3dimlem4a  39962  3dimlem4  39963  3dimlem4OLDN  39964  1cvratex  39972  hlatexch4  39980  ps-2b  39981  3atlem4  39985  llnnleat  40012  2atm  40026  ps-2c  40027  llnmlplnN  40038  lplnnlelln  40042  2atmat  40060  lvoli2  40080  lvolnlelln  40083  4atlem3b  40097  4atlem10  40105  4atlem11a  40106  4atlem11b  40107  4atlem12a  40109  lplncvrlvol2  40114  2lplnja  40118  dalemswapyz  40155  lneq2at  40277  2lnat  40283  cdlema1N  40290  cdlemb  40293  paddasslem15  40333  pmodlem1  40345  llnmod2i2  40362  llnexchb2lem  40367  dalawlem1  40370  dalawlem3  40372  dalawlem4  40373  dalawlem6  40375  dalawlem7  40376  dalawlem9  40378  dalawlem10  40379  dalawlem11  40380  dalawlem12  40381  dalawlem13  40382  dalawlem15  40384  osumcllem5N  40459  osumcllem6N  40460  osumcllem7N  40461  osumcllem9N  40463  osumcllem10N  40464  osumcllem11N  40465  pl42lem1N  40478  lhpmcvr5N  40526  lhp2atne  40533  lhp2at0ne  40535  4atexlempw  40548  4atexlemex6  40573  4atexlem7  40574  ldilco  40615  ltrneq  40648  trlval2  40662  trlnidat  40672  cdlemd7  40703  cdleme7aa  40741  cdleme7c  40744  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme7  40748  cdleme11c  40760  cdleme11e  40762  cdleme11l  40768  cdleme11  40769  cdleme14  40772  cdleme15a  40773  cdleme15c  40775  cdleme16b  40778  cdleme16c  40779  cdleme16d  40780  cdleme16e  40781  cdleme16f  40782  cdleme0nex  40789  cdleme18d  40794  cdleme19b  40803  cdleme19d  40805  cdleme19e  40806  cdleme20f  40813  cdleme20k  40818  cdleme20l1  40819  cdleme20l2  40820  cdleme20l  40821  cdleme20m  40822  cdleme21a  40824  cdleme21b  40825  cdleme21ct  40828  cdleme21d  40829  cdleme21e  40830  cdleme21f  40831  cdleme21h  40833  cdleme21i  40834  cdleme22eALTN  40844  cdleme22f2  40846  cdleme22g  40847  cdleme24  40851  cdleme25a  40852  cdleme25c  40854  cdleme25dN  40855  cdleme26e  40858  cdleme26ee  40859  cdleme26eALTN  40860  cdleme27N  40868  cdleme28a  40869  cdleme28b  40870  cdleme28  40872  cdlemefr32sn2aw  40903  cdlemefs32sn1aw  40913  cdleme43fsv1snlem  40919  cdleme41sn3a  40932  cdleme32c  40942  cdleme32e  40944  cdleme32le  40946  cdleme35a  40947  cdleme35b  40949  cdleme35c  40950  cdleme35e  40952  cdleme35f  40953  cdleme36a  40959  cdleme36m  40960  cdleme39a  40964  cdleme40m  40966  cdleme40n  40967  cdleme43bN  40989  cdleme43dN  40991  cdleme46f2g2  40992  cdleme46f2g1  40993  cdleme17d2  40994  cdleme4gfv  41006  cdlemeg49le  41010  cdlemeg46c  41012  cdlemeg46fvaw  41015  cdlemeg46nlpq  41016  cdlemeg46gfre  41031  cdleme50trn2  41050  cdleme  41059  cdlemg2idN  41095  cdlemg7fvbwN  41106  cdlemg10bALTN  41135  cdlemg10a  41139  cdlemg12d  41145  cdlemg12g  41148  cdlemg12  41149  cdlemg13a  41150  cdlemg13  41151  cdlemg17b  41161  cdlemg17dN  41162  cdlemg17dALTN  41163  cdlemg17e  41164  cdlemg17f  41165  cdlemg17i  41168  cdlemg17pq  41171  cdlemg17bq  41172  cdlemg17iqN  41173  cdlemg18d  41180  cdlemg18  41181  cdlemg19a  41182  cdlemg19  41183  cdlemg21  41185  cdlemg27a  41191  cdlemg28a  41192  cdlemg31b0N  41193  cdlemg27b  41195  cdlemg31c  41198  cdlemg33b0  41200  cdlemg33c0  41201  cdlemg28  41203  cdlemg33a  41205  cdlemg33  41210  cdlemg36  41213  ltrnco  41218  cdlemg44  41232  cdlemg47  41235  tendococl  41271  tendoplcl  41280  cdlemh1  41314  cdlemh2  41315  cdlemh  41316  cdlemi  41319  tendocan  41323  cdlemk5  41335  cdlemk6  41336  cdlemk7  41347  cdlemk11  41348  cdlemk12  41349  cdlemkole  41352  cdlemk14  41353  cdlemk15  41354  cdlemk16a  41355  cdlemk16  41356  cdlemk18  41367  cdlemk19  41368  cdlemk7u  41369  cdlemk11u  41370  cdlemk12u  41371  cdlemk21N  41372  cdlemk20  41373  cdlemkoatnle-2N  41374  cdlemk13-2N  41375  cdlemkole-2N  41376  cdlemk14-2N  41377  cdlemk15-2N  41378  cdlemk16-2N  41379  cdlemk17-2N  41380  cdlemk18-2N  41385  cdlemk19-2N  41386  cdlemk7u-2N  41387  cdlemk11u-2N  41388  cdlemk12u-2N  41389  cdlemk21-2N  41390  cdlemk20-2N  41391  cdlemk22  41392  cdlemk27-3  41406  cdlemk33N  41408  cdlemk11ta  41428  cdlemkid3N  41432  cdlemk11tc  41444  cdlemk11t  41445  cdlemk45  41446  cdlemk46  41447  cdlemk47  41448  cdlemk48  41449  cdlemk49  41450  cdlemk50  41451  cdlemk51  41452  cdlemk52  41453  cdlemk53a  41454  cdlemk55b  41459  cdlemkyyN  41461  cdlemk55u1  41464  cdlemk39u1  41466  cdlemk56  41470  cdlemm10N  41617  dihord1  41717  dihord2a  41718  dihord2b  41719  dihord10  41722  dihord4  41757  dihord5apre  41761  dihglblem2N  41793  dihjatc1  41810  dihjatc2N  41811  dihjatc3  41812  dihmeetlem15N  41820  dihmeetlem20N  41825  mapdpglem24  42203  hdmap14lem11  42377  hdmap14lem12  42378  flt4lem5  43107  mzpsubst  43204  monotuz  43393  congmul  43419  congsub  43422  ntrclsiso  44518  ntrclskb  44520  ntrclsk3  44521  infleinf  45823  mullimc  46068  mullimcf  46075  0ellimcdiv  46099  limclner  46101  sge0xaddlem2  46884  isubgr3stgrlem3  48466  lincdifsn  48922  itschlc0yqe  49258  itscnhlc0xyqsol  49263  itsclc0xyqsolr  49267  itsclquadeu  49275