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  16471  coprimeprodsq  16736  pythagtriplem4  16747  pythagtriplem13  16755  pythagtriplem14  16756  pythagtriplem16  16758  pythagtrip  16762  pceu  16774  mremre  17523  lsmpropd  19606  m2cpminvid  22697  decpmatid  22714  mply1topmatcllem  22747  cmpsublem  23343  isfil2  23800  cxple2a  26664  isosctr  26787  nolesgn2o  27639  nolesgn2ores  27640  nogesgn1o  27641  nogesgn1ores  27642  nolt02o  27663  nogt01o  27664  sltstr  27783  cofslts  27914  coinitslts  27915  cofcut2  27918  onsfi  28352  brbtwn2  28978  colinearalg  28983  ax5seg  29011  axcontlem4  29040  bayesth  34596  bnj1204  35168  bnj1279  35174  ofscom  36201  btwndiff  36221  ifscgr  36238  brofs2  36271  brifs2  36272  fscgr  36274  btwnconn1lem1  36281  btwnconn1lem2  36282  btwnconn1lem3  36283  btwnconn1lem4  36284  btwnconn1lem12  36292  seglecgr12im  36304  seglecgr12  36305  ivthALT  36529  islshpcv  39309  lkrshp  39361  lshpsmreu  39365  lshpkrlem5  39370  cvrval3  39669  4noncolr3  39709  4noncolr2  39710  4noncolr1  39711  athgt  39712  3dimlem2  39715  3dimlem3a  39716  3dimlem4a  39719  3dimlem4  39720  3dimlem4OLDN  39721  1cvratex  39729  hlatexch4  39737  ps-2b  39738  3atlem4  39742  llnnleat  39769  2atm  39783  ps-2c  39784  llnmlplnN  39795  lplnnlelln  39799  2atmat  39817  lvoli2  39837  lvolnlelln  39840  4atlem3b  39854  4atlem10  39862  4atlem11a  39863  4atlem11b  39864  4atlem12a  39866  lplncvrlvol2  39871  2lplnja  39875  dalemswapyz  39912  lneq2at  40034  2lnat  40040  cdlema1N  40047  cdlemb  40050  paddasslem15  40090  pmodlem1  40102  llnmod2i2  40119  llnexchb2lem  40124  dalawlem1  40127  dalawlem3  40129  dalawlem4  40130  dalawlem6  40132  dalawlem7  40133  dalawlem9  40135  dalawlem10  40136  dalawlem11  40137  dalawlem12  40138  dalawlem13  40139  dalawlem15  40141  osumcllem5N  40216  osumcllem6N  40217  osumcllem7N  40218  osumcllem9N  40220  osumcllem10N  40221  osumcllem11N  40222  pl42lem1N  40235  lhpmcvr5N  40283  lhp2atne  40290  lhp2at0ne  40292  4atexlempw  40305  4atexlemex6  40330  4atexlem7  40331  ldilco  40372  ltrneq  40405  trlval2  40419  trlnidat  40429  cdlemd7  40460  cdleme7aa  40498  cdleme7c  40501  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme11c  40517  cdleme11e  40519  cdleme11l  40525  cdleme11  40526  cdleme14  40529  cdleme15a  40530  cdleme15c  40532  cdleme16b  40535  cdleme16c  40536  cdleme16d  40537  cdleme16e  40538  cdleme16f  40539  cdleme0nex  40546  cdleme18d  40551  cdleme19b  40560  cdleme19d  40562  cdleme19e  40563  cdleme20f  40570  cdleme20k  40575  cdleme20l1  40576  cdleme20l2  40577  cdleme20l  40578  cdleme20m  40579  cdleme21a  40581  cdleme21b  40582  cdleme21ct  40585  cdleme21d  40586  cdleme21e  40587  cdleme21f  40588  cdleme21h  40590  cdleme21i  40591  cdleme22eALTN  40601  cdleme22f2  40603  cdleme22g  40604  cdleme24  40608  cdleme25a  40609  cdleme25c  40611  cdleme25dN  40612  cdleme26e  40615  cdleme26ee  40616  cdleme26eALTN  40617  cdleme27N  40625  cdleme28a  40626  cdleme28b  40627  cdleme28  40629  cdlemefr32sn2aw  40660  cdlemefs32sn1aw  40670  cdleme43fsv1snlem  40676  cdleme41sn3a  40689  cdleme32c  40699  cdleme32e  40701  cdleme32le  40703  cdleme35a  40704  cdleme35b  40706  cdleme35c  40707  cdleme35e  40709  cdleme35f  40710  cdleme36a  40716  cdleme36m  40717  cdleme39a  40721  cdleme40m  40723  cdleme40n  40724  cdleme43bN  40746  cdleme43dN  40748  cdleme46f2g2  40749  cdleme46f2g1  40750  cdleme17d2  40751  cdleme4gfv  40763  cdlemeg49le  40767  cdlemeg46c  40769  cdlemeg46fvaw  40772  cdlemeg46nlpq  40773  cdlemeg46gfre  40788  cdleme50trn2  40807  cdleme  40816  cdlemg2idN  40852  cdlemg7fvbwN  40863  cdlemg10bALTN  40892  cdlemg10a  40896  cdlemg12d  40902  cdlemg12g  40905  cdlemg12  40906  cdlemg13a  40907  cdlemg13  40908  cdlemg17b  40918  cdlemg17dN  40919  cdlemg17dALTN  40920  cdlemg17e  40921  cdlemg17f  40922  cdlemg17i  40925  cdlemg17pq  40928  cdlemg17bq  40929  cdlemg17iqN  40930  cdlemg18d  40937  cdlemg18  40938  cdlemg19a  40939  cdlemg19  40940  cdlemg21  40942  cdlemg27a  40948  cdlemg28a  40949  cdlemg31b0N  40950  cdlemg27b  40952  cdlemg31c  40955  cdlemg33b0  40957  cdlemg33c0  40958  cdlemg28  40960  cdlemg33a  40962  cdlemg33  40967  cdlemg36  40970  ltrnco  40975  cdlemg44  40989  cdlemg47  40992  tendococl  41028  tendoplcl  41037  cdlemh1  41071  cdlemh2  41072  cdlemh  41073  cdlemi  41076  tendocan  41080  cdlemk5  41092  cdlemk6  41093  cdlemk7  41104  cdlemk11  41105  cdlemk12  41106  cdlemkole  41109  cdlemk14  41110  cdlemk15  41111  cdlemk16a  41112  cdlemk16  41113  cdlemk18  41124  cdlemk19  41125  cdlemk7u  41126  cdlemk11u  41127  cdlemk12u  41128  cdlemk21N  41129  cdlemk20  41130  cdlemkoatnle-2N  41131  cdlemk13-2N  41132  cdlemkole-2N  41133  cdlemk14-2N  41134  cdlemk15-2N  41135  cdlemk16-2N  41136  cdlemk17-2N  41137  cdlemk18-2N  41142  cdlemk19-2N  41143  cdlemk7u-2N  41144  cdlemk11u-2N  41145  cdlemk12u-2N  41146  cdlemk21-2N  41147  cdlemk20-2N  41148  cdlemk22  41149  cdlemk27-3  41163  cdlemk33N  41165  cdlemk11ta  41185  cdlemkid3N  41189  cdlemk11tc  41201  cdlemk11t  41202  cdlemk45  41203  cdlemk46  41204  cdlemk47  41205  cdlemk48  41206  cdlemk49  41207  cdlemk50  41208  cdlemk51  41209  cdlemk52  41210  cdlemk53a  41211  cdlemk55b  41216  cdlemkyyN  41218  cdlemk55u1  41221  cdlemk39u1  41223  cdlemk56  41227  cdlemm10N  41374  dihord1  41474  dihord2a  41475  dihord2b  41476  dihord10  41479  dihord4  41514  dihord5apre  41518  dihglblem2N  41550  dihjatc1  41567  dihjatc2N  41568  dihjatc3  41569  dihmeetlem15N  41577  dihmeetlem20N  41582  mapdpglem24  41960  hdmap14lem11  42134  hdmap14lem12  42135  flt4lem5  42889  mzpsubst  42986  monotuz  43179  congmul  43205  congsub  43208  ntrclsiso  44304  ntrclskb  44306  ntrclsk3  44307  infleinf  45612  mullimc  45858  mullimcf  45865  0ellimcdiv  45889  limclner  45891  sge0xaddlem2  46674  isubgr3stgrlem3  48210  lincdifsn  48666  itschlc0yqe  49002  itscnhlc0xyqsol  49007  itsclc0xyqsolr  49011  itsclquadeu  49019