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  16746  coprimeprodsq  17015  pythagtriplem4  17026  pythagtriplem13  17034  pythagtriplem14  17035  pythagtriplem16  17037  pythagtrip  17041  pceu  17053  mremre  17803  lsmpropd  19921  m2cpminvid  23101  decpmatid  23118  mply1topmatcllem  23151  cmpsublem  23747  isfil2  24205  cxple2a  27057  isosctr  27179  flt4lem5  28010  nolesgn2o  28058  nolesgn2ores  28059  nogesgn1o  28060  nogesgn1ores  28061  nolt02o  28082  nogt01o  28083  sltstr  28203  cofslts  28334  coinitslts  28335  cofcut2  28338  onsfi  28772  brbtwn2  29513  colinearalg  29518  ax5seg  29546  axcontlem4  29575  bayesth  35141  bnj1204  35712  bnj1279  35718  ofscom  36950  btwndiff  36970  ifscgr  36987  brofs2  37020  brifs2  37021  fscgr  37023  btwnconn1lem1  37030  btwnconn1lem2  37031  btwnconn1lem3  37032  btwnconn1lem4  37033  btwnconn1lem12  37041  seglecgr12im  37053  seglecgr12  37054  ivthALT  37301  islshpcv  40302  lkrshp  40354  lshpsmreu  40358  lshpkrlem5  40363  cvrval3  40662  4noncolr3  40702  4noncolr2  40703  4noncolr1  40704  athgt  40705  3dimlem2  40708  3dimlem3a  40709  3dimlem4a  40712  3dimlem4  40713  3dimlem4OLDN  40714  1cvratex  40722  hlatexch4  40730  ps-2b  40731  3atlem4  40735  llnnleat  40762  2atm  40776  ps-2c  40777  llnmlplnN  40788  lplnnlelln  40792  2atmat  40810  lvoli2  40830  lvolnlelln  40833  4atlem3b  40847  4atlem10  40855  4atlem11a  40856  4atlem11b  40857  4atlem12a  40859  lplncvrlvol2  40864  2lplnja  40868  dalemswapyz  40905  lneq2at  41027  2lnat  41033  cdlema1N  41040  cdlemb  41043  paddasslem15  41083  pmodlem1  41095  llnmod2i2  41112  llnexchb2lem  41117  dalawlem1  41120  dalawlem3  41122  dalawlem4  41123  dalawlem6  41125  dalawlem7  41126  dalawlem9  41128  dalawlem10  41129  dalawlem11  41130  dalawlem12  41131  dalawlem13  41132  dalawlem15  41134  osumcllem5N  41209  osumcllem6N  41210  osumcllem7N  41211  osumcllem9N  41213  osumcllem10N  41214  osumcllem11N  41215  pl42lem1N  41228  lhpmcvr5N  41276  lhp2atne  41283  lhp2at0ne  41285  4atexlempw  41298  4atexlemex6  41323  4atexlem7  41324  ldilco  41365  ltrneq  41398  trlval2  41412  trlnidat  41422  cdlemd7  41453  cdleme7aa  41491  cdleme7c  41494  cdleme7d  41495  cdleme7e  41496  cdleme7ga  41497  cdleme7  41498  cdleme11c  41510  cdleme11e  41512  cdleme11l  41518  cdleme11  41519  cdleme14  41522  cdleme15a  41523  cdleme15c  41525  cdleme16b  41528  cdleme16c  41529  cdleme16d  41530  cdleme16e  41531  cdleme16f  41532  cdleme0nex  41539  cdleme18d  41544  cdleme19b  41553  cdleme19d  41555  cdleme19e  41556  cdleme20f  41563  cdleme20k  41568  cdleme20l1  41569  cdleme20l2  41570  cdleme20l  41571  cdleme20m  41572  cdleme21a  41574  cdleme21b  41575  cdleme21ct  41578  cdleme21d  41579  cdleme21e  41580  cdleme21f  41581  cdleme21h  41583  cdleme21i  41584  cdleme22eALTN  41594  cdleme22f2  41596  cdleme22g  41597  cdleme24  41601  cdleme25a  41602  cdleme25c  41604  cdleme25dN  41605  cdleme26e  41608  cdleme26ee  41609  cdleme26eALTN  41610  cdleme27N  41618  cdleme28a  41619  cdleme28b  41620  cdleme28  41622  cdlemefr32sn2aw  41653  cdlemefs32sn1aw  41663  cdleme43fsv1snlem  41669  cdleme41sn3a  41682  cdleme32c  41692  cdleme32e  41694  cdleme32le  41696  cdleme35a  41697  cdleme35b  41699  cdleme35c  41700  cdleme35e  41702  cdleme35f  41703  cdleme36a  41709  cdleme36m  41710  cdleme39a  41714  cdleme40m  41716  cdleme40n  41717  cdleme43bN  41739  cdleme43dN  41741  cdleme46f2g2  41742  cdleme46f2g1  41743  cdleme17d2  41744  cdleme4gfv  41756  cdlemeg49le  41760  cdlemeg46c  41762  cdlemeg46fvaw  41765  cdlemeg46nlpq  41766  cdlemeg46gfre  41781  cdleme50trn2  41800  cdleme  41809  cdlemg2idN  41845  cdlemg7fvbwN  41856  cdlemg10bALTN  41885  cdlemg10a  41889  cdlemg12d  41895  cdlemg12g  41898  cdlemg12  41899  cdlemg13a  41900  cdlemg13  41901  cdlemg17b  41911  cdlemg17dN  41912  cdlemg17dALTN  41913  cdlemg17e  41914  cdlemg17f  41915  cdlemg17i  41918  cdlemg17pq  41921  cdlemg17bq  41922  cdlemg17iqN  41923  cdlemg18d  41930  cdlemg18  41931  cdlemg19a  41932  cdlemg19  41933  cdlemg21  41935  cdlemg27a  41941  cdlemg28a  41942  cdlemg31b0N  41943  cdlemg27b  41945  cdlemg31c  41948  cdlemg33b0  41950  cdlemg33c0  41951  cdlemg28  41953  cdlemg33a  41955  cdlemg33  41960  cdlemg36  41963  ltrnco  41968  cdlemg44  41982  cdlemg47  41985  tendococl  42021  tendoplcl  42030  cdlemh1  42064  cdlemh2  42065  cdlemh  42066  cdlemi  42069  tendocan  42073  cdlemk5  42085  cdlemk6  42086  cdlemk7  42097  cdlemk11  42098  cdlemk12  42099  cdlemkole  42102  cdlemk14  42103  cdlemk15  42104  cdlemk16a  42105  cdlemk16  42106  cdlemk18  42117  cdlemk19  42118  cdlemk7u  42119  cdlemk11u  42120  cdlemk12u  42121  cdlemk21N  42122  cdlemk20  42123  cdlemkoatnle-2N  42124  cdlemk13-2N  42125  cdlemkole-2N  42126  cdlemk14-2N  42127  cdlemk15-2N  42128  cdlemk16-2N  42129  cdlemk17-2N  42130  cdlemk18-2N  42135  cdlemk19-2N  42136  cdlemk7u-2N  42137  cdlemk11u-2N  42138  cdlemk12u-2N  42139  cdlemk21-2N  42140  cdlemk20-2N  42141  cdlemk22  42142  cdlemk27-3  42156  cdlemk33N  42158  cdlemk11ta  42178  cdlemkid3N  42182  cdlemk11tc  42194  cdlemk11t  42195  cdlemk45  42196  cdlemk46  42197  cdlemk47  42198  cdlemk48  42199  cdlemk49  42200  cdlemk50  42201  cdlemk51  42202  cdlemk52  42203  cdlemk53a  42204  cdlemk55b  42209  cdlemkyyN  42211  cdlemk55u1  42214  cdlemk39u1  42216  cdlemk56  42220  cdlemm10N  42367  dihord1  42467  dihord2a  42468  dihord2b  42469  dihord10  42472  dihord4  42507  dihord5apre  42511  dihglblem2N  42543  dihjatc1  42560  dihjatc2N  42561  dihjatc3  42562  dihmeetlem15N  42570  dihmeetlem20N  42575  mapdpglem24  42953  hdmap14lem11  43127  hdmap14lem12  43128  mzpsubst  43952  monotuz  44141  congmul  44167  congsub  44170  ntrclsiso  45259  ntrclskb  45261  ntrclsk3  45262  infleinf  46588  mullimc  46833  mullimcf  46840  0ellimcdiv  46864  limclner  46866  sge0xaddlem2  47649  isubgr3stgrlem3  49271  lincdifsn  49741  itschlc0yqe  50077  itscnhlc0xyqsol  50082  itsclc0xyqsolr  50086  itsclquadeu  50094