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  16697  coprimeprodsq  16966  pythagtriplem4  16977  pythagtriplem13  16985  pythagtriplem14  16986  pythagtriplem16  16988  pythagtrip  16992  pceu  17004  mremre  17754  lsmpropd  19871  m2cpminvid  23051  decpmatid  23068  mply1topmatcllem  23101  cmpsublem  23697  isfil2  24155  cxple2a  27009  isosctr  27131  flt4lem5  27962  nolesgn2o  28010  nolesgn2ores  28011  nogesgn1o  28012  nogesgn1ores  28013  nolt02o  28034  nogt01o  28035  sltstr  28155  cofslts  28286  coinitslts  28287  cofcut2  28290  onsfi  28724  brbtwn2  29465  colinearalg  29470  ax5seg  29498  axcontlem4  29527  bayesth  35054  bnj1204  35625  bnj1279  35631  ofscom  36742  btwndiff  36762  ifscgr  36779  brofs2  36812  brifs2  36813  fscgr  36815  btwnconn1lem1  36822  btwnconn1lem2  36823  btwnconn1lem3  36824  btwnconn1lem4  36825  btwnconn1lem12  36833  seglecgr12im  36845  seglecgr12  36846  ivthALT  37093  islshpcv  40078  lkrshp  40130  lshpsmreu  40134  lshpkrlem5  40139  cvrval3  40438  4noncolr3  40478  4noncolr2  40479  4noncolr1  40480  athgt  40481  3dimlem2  40484  3dimlem3a  40485  3dimlem4a  40488  3dimlem4  40489  3dimlem4OLDN  40490  1cvratex  40498  hlatexch4  40506  ps-2b  40507  3atlem4  40511  llnnleat  40538  2atm  40552  ps-2c  40553  llnmlplnN  40564  lplnnlelln  40568  2atmat  40586  lvoli2  40606  lvolnlelln  40609  4atlem3b  40623  4atlem10  40631  4atlem11a  40632  4atlem11b  40633  4atlem12a  40635  lplncvrlvol2  40640  2lplnja  40644  dalemswapyz  40681  lneq2at  40803  2lnat  40809  cdlema1N  40816  cdlemb  40819  paddasslem15  40859  pmodlem1  40871  llnmod2i2  40888  llnexchb2lem  40893  dalawlem1  40896  dalawlem3  40898  dalawlem4  40899  dalawlem6  40901  dalawlem7  40902  dalawlem9  40904  dalawlem10  40905  dalawlem11  40906  dalawlem12  40907  dalawlem13  40908  dalawlem15  40910  osumcllem5N  40985  osumcllem6N  40986  osumcllem7N  40987  osumcllem9N  40989  osumcllem10N  40990  osumcllem11N  40991  pl42lem1N  41004  lhpmcvr5N  41052  lhp2atne  41059  lhp2at0ne  41061  4atexlempw  41074  4atexlemex6  41099  4atexlem7  41100  ldilco  41141  ltrneq  41174  trlval2  41188  trlnidat  41198  cdlemd7  41229  cdleme7aa  41267  cdleme7c  41270  cdleme7d  41271  cdleme7e  41272  cdleme7ga  41273  cdleme7  41274  cdleme11c  41286  cdleme11e  41288  cdleme11l  41294  cdleme11  41295  cdleme14  41298  cdleme15a  41299  cdleme15c  41301  cdleme16b  41304  cdleme16c  41305  cdleme16d  41306  cdleme16e  41307  cdleme16f  41308  cdleme0nex  41315  cdleme18d  41320  cdleme19b  41329  cdleme19d  41331  cdleme19e  41332  cdleme20f  41339  cdleme20k  41344  cdleme20l1  41345  cdleme20l2  41346  cdleme20l  41347  cdleme20m  41348  cdleme21a  41350  cdleme21b  41351  cdleme21ct  41354  cdleme21d  41355  cdleme21e  41356  cdleme21f  41357  cdleme21h  41359  cdleme21i  41360  cdleme22eALTN  41370  cdleme22f2  41372  cdleme22g  41373  cdleme24  41377  cdleme25a  41378  cdleme25c  41380  cdleme25dN  41381  cdleme26e  41384  cdleme26ee  41385  cdleme26eALTN  41386  cdleme27N  41394  cdleme28a  41395  cdleme28b  41396  cdleme28  41398  cdlemefr32sn2aw  41429  cdlemefs32sn1aw  41439  cdleme43fsv1snlem  41445  cdleme41sn3a  41458  cdleme32c  41468  cdleme32e  41470  cdleme32le  41472  cdleme35a  41473  cdleme35b  41475  cdleme35c  41476  cdleme35e  41478  cdleme35f  41479  cdleme36a  41485  cdleme36m  41486  cdleme39a  41490  cdleme40m  41492  cdleme40n  41493  cdleme43bN  41515  cdleme43dN  41517  cdleme46f2g2  41518  cdleme46f2g1  41519  cdleme17d2  41520  cdleme4gfv  41532  cdlemeg49le  41536  cdlemeg46c  41538  cdlemeg46fvaw  41541  cdlemeg46nlpq  41542  cdlemeg46gfre  41557  cdleme50trn2  41576  cdleme  41585  cdlemg2idN  41621  cdlemg7fvbwN  41632  cdlemg10bALTN  41661  cdlemg10a  41665  cdlemg12d  41671  cdlemg12g  41674  cdlemg12  41675  cdlemg13a  41676  cdlemg13  41677  cdlemg17b  41687  cdlemg17dN  41688  cdlemg17dALTN  41689  cdlemg17e  41690  cdlemg17f  41691  cdlemg17i  41694  cdlemg17pq  41697  cdlemg17bq  41698  cdlemg17iqN  41699  cdlemg18d  41706  cdlemg18  41707  cdlemg19a  41708  cdlemg19  41709  cdlemg21  41711  cdlemg27a  41717  cdlemg28a  41718  cdlemg31b0N  41719  cdlemg27b  41721  cdlemg31c  41724  cdlemg33b0  41726  cdlemg33c0  41727  cdlemg28  41729  cdlemg33a  41731  cdlemg33  41736  cdlemg36  41739  ltrnco  41744  cdlemg44  41758  cdlemg47  41761  tendococl  41797  tendoplcl  41806  cdlemh1  41840  cdlemh2  41841  cdlemh  41842  cdlemi  41845  tendocan  41849  cdlemk5  41861  cdlemk6  41862  cdlemk7  41873  cdlemk11  41874  cdlemk12  41875  cdlemkole  41878  cdlemk14  41879  cdlemk15  41880  cdlemk16a  41881  cdlemk16  41882  cdlemk18  41893  cdlemk19  41894  cdlemk7u  41895  cdlemk11u  41896  cdlemk12u  41897  cdlemk21N  41898  cdlemk20  41899  cdlemkoatnle-2N  41900  cdlemk13-2N  41901  cdlemkole-2N  41902  cdlemk14-2N  41903  cdlemk15-2N  41904  cdlemk16-2N  41905  cdlemk17-2N  41906  cdlemk18-2N  41911  cdlemk19-2N  41912  cdlemk7u-2N  41913  cdlemk11u-2N  41914  cdlemk12u-2N  41915  cdlemk21-2N  41916  cdlemk20-2N  41917  cdlemk22  41918  cdlemk27-3  41932  cdlemk33N  41934  cdlemk11ta  41954  cdlemkid3N  41958  cdlemk11tc  41970  cdlemk11t  41971  cdlemk45  41972  cdlemk46  41973  cdlemk47  41974  cdlemk48  41975  cdlemk49  41976  cdlemk50  41977  cdlemk51  41978  cdlemk52  41979  cdlemk53a  41980  cdlemk55b  41985  cdlemkyyN  41987  cdlemk55u1  41990  cdlemk39u1  41992  cdlemk56  41996  cdlemm10N  42143  dihord1  42243  dihord2a  42244  dihord2b  42245  dihord10  42248  dihord4  42283  dihord5apre  42287  dihglblem2N  42319  dihjatc1  42336  dihjatc2N  42337  dihjatc3  42338  dihmeetlem15N  42346  dihmeetlem20N  42351  mapdpglem24  42729  hdmap14lem11  42903  hdmap14lem12  42904  mzpsubst  43712  monotuz  43901  congmul  43927  congsub  43930  ntrclsiso  45026  ntrclskb  45028  ntrclsk3  45029  infleinf  46327  mullimc  46572  mullimcf  46579  0ellimcdiv  46603  limclner  46605  sge0xaddlem2  47388  isubgr3stgrlem3  49010  lincdifsn  49480  itschlc0yqe  49816  itscnhlc0xyqsol  49821  itsclc0xyqsolr  49825  itsclquadeu  49833