Theorem simp12 1206

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  simp112  1305  simp212  1314  simp312  1323  dvdsgcd  16483  coprimeprodsq  16748  pythagtriplem4  16759  pythagtriplem13  16767  pythagtriplem14  16768  pythagtriplem16  16770  pythagtrip  16774  pceu  16786  mremre  17535  lsmpropd  19618  m2cpminvid  22709  decpmatid  22726  mply1topmatcllem  22759  cmpsublem  23355  isfil2  23812  cxple2a  26676  isosctr  26799  nolesgn2o  27651  nolesgn2ores  27652  nogesgn1o  27653  nogesgn1ores  27654  nolt02o  27675  nogt01o  27676  sltstr  27795  cofslts  27926  coinitslts  27927  cofcut2  27930  onsfi  28364  brbtwn2  28990  colinearalg  28995  ax5seg  29023  axcontlem4  29052  bayesth  34616  bnj1204  35187  bnj1279  35193  ofscom  36220  btwndiff  36240  ifscgr  36257  brofs2  36290  brifs2  36291  fscgr  36293  btwnconn1lem1  36300  btwnconn1lem2  36301  btwnconn1lem3  36302  btwnconn1lem4  36303  btwnconn1lem12  36311  seglecgr12im  36323  seglecgr12  36324  ivthALT  36548  islshpcv  39423  lkrshp  39475  lshpsmreu  39479  lshpkrlem5  39484  cvrval3  39783  4noncolr3  39823  4noncolr2  39824  4noncolr1  39825  athgt  39826  3dimlem2  39829  3dimlem3a  39830  3dimlem4a  39833  3dimlem4  39834  3dimlem4OLDN  39835  1cvratex  39843  hlatexch4  39851  ps-2b  39852  3atlem4  39856  llnnleat  39883  2atm  39897  ps-2c  39898  llnmlplnN  39909  lplnnlelln  39913  2atmat  39931  lvoli2  39951  lvolnlelln  39954  4atlem3b  39968  4atlem10  39976  4atlem11a  39977  4atlem11b  39978  4atlem12a  39980  lplncvrlvol2  39985  2lplnja  39989  dalemswapyz  40026  lneq2at  40148  2lnat  40154  cdlema1N  40161  cdlemb  40164  paddasslem15  40204  pmodlem1  40216  llnmod2i2  40233  llnexchb2lem  40238  dalawlem1  40241  dalawlem3  40243  dalawlem4  40244  dalawlem6  40246  dalawlem7  40247  dalawlem9  40249  dalawlem10  40250  dalawlem11  40251  dalawlem12  40252  dalawlem13  40253  dalawlem15  40255  osumcllem5N  40330  osumcllem6N  40331  osumcllem7N  40332  osumcllem9N  40334  osumcllem10N  40335  osumcllem11N  40336  pl42lem1N  40349  lhpmcvr5N  40397  lhp2atne  40404  lhp2at0ne  40406  4atexlempw  40419  4atexlemex6  40444  4atexlem7  40445  ldilco  40486  ltrneq  40519  trlval2  40533  trlnidat  40543  cdlemd7  40574  cdleme7aa  40612  cdleme7c  40615  cdleme7d  40616  cdleme7e  40617  cdleme7ga  40618  cdleme7  40619  cdleme11c  40631  cdleme11e  40633  cdleme11l  40639  cdleme11  40640  cdleme14  40643  cdleme15a  40644  cdleme15c  40646  cdleme16b  40649  cdleme16c  40650  cdleme16d  40651  cdleme16e  40652  cdleme16f  40653  cdleme0nex  40660  cdleme18d  40665  cdleme19b  40674  cdleme19d  40676  cdleme19e  40677  cdleme20f  40684  cdleme20k  40689  cdleme20l1  40690  cdleme20l2  40691  cdleme20l  40692  cdleme20m  40693  cdleme21a  40695  cdleme21b  40696  cdleme21ct  40699  cdleme21d  40700  cdleme21e  40701  cdleme21f  40702  cdleme21h  40704  cdleme21i  40705  cdleme22eALTN  40715  cdleme22f2  40717  cdleme22g  40718  cdleme24  40722  cdleme25a  40723  cdleme25c  40725  cdleme25dN  40726  cdleme26e  40729  cdleme26ee  40730  cdleme26eALTN  40731  cdleme27N  40739  cdleme28a  40740  cdleme28b  40741  cdleme28  40743  cdlemefr32sn2aw  40774  cdlemefs32sn1aw  40784  cdleme43fsv1snlem  40790  cdleme41sn3a  40803  cdleme32c  40813  cdleme32e  40815  cdleme32le  40817  cdleme35a  40818  cdleme35b  40820  cdleme35c  40821  cdleme35e  40823  cdleme35f  40824  cdleme36a  40830  cdleme36m  40831  cdleme39a  40835  cdleme40m  40837  cdleme40n  40838  cdleme43bN  40860  cdleme43dN  40862  cdleme46f2g2  40863  cdleme46f2g1  40864  cdleme17d2  40865  cdleme4gfv  40877  cdlemeg49le  40881  cdlemeg46c  40883  cdlemeg46fvaw  40886  cdlemeg46nlpq  40887  cdlemeg46gfre  40902  cdleme50trn2  40921  cdleme  40930  cdlemg2idN  40966  cdlemg7fvbwN  40977  cdlemg10bALTN  41006  cdlemg10a  41010  cdlemg12d  41016  cdlemg12g  41019  cdlemg12  41020  cdlemg13a  41021  cdlemg13  41022  cdlemg17b  41032  cdlemg17dN  41033  cdlemg17dALTN  41034  cdlemg17e  41035  cdlemg17f  41036  cdlemg17i  41039  cdlemg17pq  41042  cdlemg17bq  41043  cdlemg17iqN  41044  cdlemg18d  41051  cdlemg18  41052  cdlemg19a  41053  cdlemg19  41054  cdlemg21  41056  cdlemg27a  41062  cdlemg28a  41063  cdlemg31b0N  41064  cdlemg27b  41066  cdlemg31c  41069  cdlemg33b0  41071  cdlemg33c0  41072  cdlemg28  41074  cdlemg33a  41076  cdlemg33  41081  cdlemg36  41084  ltrnco  41089  cdlemg44  41103  cdlemg47  41106  tendococl  41142  tendoplcl  41151  cdlemh1  41185  cdlemh2  41186  cdlemh  41187  cdlemi  41190  tendocan  41194  cdlemk5  41206  cdlemk6  41207  cdlemk7  41218  cdlemk11  41219  cdlemk12  41220  cdlemkole  41223  cdlemk14  41224  cdlemk15  41225  cdlemk16a  41226  cdlemk16  41227  cdlemk18  41238  cdlemk19  41239  cdlemk7u  41240  cdlemk11u  41241  cdlemk12u  41242  cdlemk21N  41243  cdlemk20  41244  cdlemkoatnle-2N  41245  cdlemk13-2N  41246  cdlemkole-2N  41247  cdlemk14-2N  41248  cdlemk15-2N  41249  cdlemk16-2N  41250  cdlemk17-2N  41251  cdlemk18-2N  41256  cdlemk19-2N  41257  cdlemk7u-2N  41258  cdlemk11u-2N  41259  cdlemk12u-2N  41260  cdlemk21-2N  41261  cdlemk20-2N  41262  cdlemk22  41263  cdlemk27-3  41277  cdlemk33N  41279  cdlemk11ta  41299  cdlemkid3N  41303  cdlemk11tc  41315  cdlemk11t  41316  cdlemk45  41317  cdlemk46  41318  cdlemk47  41319  cdlemk48  41320  cdlemk49  41321  cdlemk50  41322  cdlemk51  41323  cdlemk52  41324  cdlemk53a  41325  cdlemk55b  41330  cdlemkyyN  41332  cdlemk55u1  41335  cdlemk39u1  41337  cdlemk56  41341  cdlemm10N  41488  dihord1  41588  dihord2a  41589  dihord2b  41590  dihord10  41593  dihord4  41628  dihord5apre  41632  dihglblem2N  41664  dihjatc1  41681  dihjatc2N  41682  dihjatc3  41683  dihmeetlem15N  41691  dihmeetlem20N  41696  mapdpglem24  42074  hdmap14lem11  42248  hdmap14lem12  42249  flt4lem5  43002  mzpsubst  43099  monotuz  43292  congmul  43318  congsub  43321  ntrclsiso  44417  ntrclskb  44419  ntrclsk3  44420  infleinf  45724  mullimc  45970  mullimcf  45977  0ellimcdiv  46001  limclner  46003  sge0xaddlem2  46786  isubgr3stgrlem3  48322  lincdifsn  48778  itschlc0yqe  49114  itscnhlc0xyqsol  49119  itsclc0xyqsolr  49123  itsclquadeu  49131