Theorem simp12 1221

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simp112  1320  simp212  1329  simp312  1338  dvdsgcd  16592  coprimeprodsq  16858  pythagtriplem4  16869  pythagtriplem13  16877  pythagtriplem14  16878  pythagtriplem16  16880  pythagtrip  16884  pceu  16896  mremre  17646  lsmpropd  19738  m2cpminvid  22871  decpmatid  22888  mply1topmatcllem  22921  cmpsublem  23517  isfil2  23974  cxple2a  26822  isosctr  26944  nolesgn2o  27793  nolesgn2ores  27794  nogesgn1o  27795  nogesgn1ores  27796  nolt02o  27817  nogt01o  27818  sltstr  27938  cofslts  28069  coinitslts  28070  cofcut2  28073  onsfi  28507  brbtwn2  29164  colinearalg  29169  ax5seg  29197  axcontlem4  29226  bayesth  34746  bnj1204  35317  bnj1279  35323  ofscom  36370  btwndiff  36390  ifscgr  36407  brofs2  36440  brifs2  36441  fscgr  36443  btwnconn1lem1  36450  btwnconn1lem2  36451  btwnconn1lem3  36452  btwnconn1lem4  36453  btwnconn1lem12  36461  seglecgr12im  36473  seglecgr12  36474  ivthALT  36708  islshpcv  39689  lkrshp  39741  lshpsmreu  39745  lshpkrlem5  39750  cvrval3  40049  4noncolr3  40089  4noncolr2  40090  4noncolr1  40091  athgt  40092  3dimlem2  40095  3dimlem3a  40096  3dimlem4a  40099  3dimlem4  40100  3dimlem4OLDN  40101  1cvratex  40109  hlatexch4  40117  ps-2b  40118  3atlem4  40122  llnnleat  40149  2atm  40163  ps-2c  40164  llnmlplnN  40175  lplnnlelln  40179  2atmat  40197  lvoli2  40217  lvolnlelln  40220  4atlem3b  40234  4atlem10  40242  4atlem11a  40243  4atlem11b  40244  4atlem12a  40246  lplncvrlvol2  40251  2lplnja  40255  dalemswapyz  40292  lneq2at  40414  2lnat  40420  cdlema1N  40427  cdlemb  40430  paddasslem15  40470  pmodlem1  40482  llnmod2i2  40499  llnexchb2lem  40504  dalawlem1  40507  dalawlem3  40509  dalawlem4  40510  dalawlem6  40512  dalawlem7  40513  dalawlem9  40515  dalawlem10  40516  dalawlem11  40517  dalawlem12  40518  dalawlem13  40519  dalawlem15  40521  osumcllem5N  40596  osumcllem6N  40597  osumcllem7N  40598  osumcllem9N  40600  osumcllem10N  40601  osumcllem11N  40602  pl42lem1N  40615  lhpmcvr5N  40663  lhp2atne  40670  lhp2at0ne  40672  4atexlempw  40685  4atexlemex6  40710  4atexlem7  40711  ldilco  40752  ltrneq  40785  trlval2  40799  trlnidat  40809  cdlemd7  40840  cdleme7aa  40878  cdleme7c  40881  cdleme7d  40882  cdleme7e  40883  cdleme7ga  40884  cdleme7  40885  cdleme11c  40897  cdleme11e  40899  cdleme11l  40905  cdleme11  40906  cdleme14  40909  cdleme15a  40910  cdleme15c  40912  cdleme16b  40915  cdleme16c  40916  cdleme16d  40917  cdleme16e  40918  cdleme16f  40919  cdleme0nex  40926  cdleme18d  40931  cdleme19b  40940  cdleme19d  40942  cdleme19e  40943  cdleme20f  40950  cdleme20k  40955  cdleme20l1  40956  cdleme20l2  40957  cdleme20l  40958  cdleme20m  40959  cdleme21a  40961  cdleme21b  40962  cdleme21ct  40965  cdleme21d  40966  cdleme21e  40967  cdleme21f  40968  cdleme21h  40970  cdleme21i  40971  cdleme22eALTN  40981  cdleme22f2  40983  cdleme22g  40984  cdleme24  40988  cdleme25a  40989  cdleme25c  40991  cdleme25dN  40992  cdleme26e  40995  cdleme26ee  40996  cdleme26eALTN  40997  cdleme27N  41005  cdleme28a  41006  cdleme28b  41007  cdleme28  41009  cdlemefr32sn2aw  41040  cdlemefs32sn1aw  41050  cdleme43fsv1snlem  41056  cdleme41sn3a  41069  cdleme32c  41079  cdleme32e  41081  cdleme32le  41083  cdleme35a  41084  cdleme35b  41086  cdleme35c  41087  cdleme35e  41089  cdleme35f  41090  cdleme36a  41096  cdleme36m  41097  cdleme39a  41101  cdleme40m  41103  cdleme40n  41104  cdleme43bN  41126  cdleme43dN  41128  cdleme46f2g2  41129  cdleme46f2g1  41130  cdleme17d2  41131  cdleme4gfv  41143  cdlemeg49le  41147  cdlemeg46c  41149  cdlemeg46fvaw  41152  cdlemeg46nlpq  41153  cdlemeg46gfre  41168  cdleme50trn2  41187  cdleme  41196  cdlemg2idN  41232  cdlemg7fvbwN  41243  cdlemg10bALTN  41272  cdlemg10a  41276  cdlemg12d  41282  cdlemg12g  41285  cdlemg12  41286  cdlemg13a  41287  cdlemg13  41288  cdlemg17b  41298  cdlemg17dN  41299  cdlemg17dALTN  41300  cdlemg17e  41301  cdlemg17f  41302  cdlemg17i  41305  cdlemg17pq  41308  cdlemg17bq  41309  cdlemg17iqN  41310  cdlemg18d  41317  cdlemg18  41318  cdlemg19a  41319  cdlemg19  41320  cdlemg21  41322  cdlemg27a  41328  cdlemg28a  41329  cdlemg31b0N  41330  cdlemg27b  41332  cdlemg31c  41335  cdlemg33b0  41337  cdlemg33c0  41338  cdlemg28  41340  cdlemg33a  41342  cdlemg33  41347  cdlemg36  41350  ltrnco  41355  cdlemg44  41369  cdlemg47  41372  tendococl  41408  tendoplcl  41417  cdlemh1  41451  cdlemh2  41452  cdlemh  41453  cdlemi  41456  tendocan  41460  cdlemk5  41472  cdlemk6  41473  cdlemk7  41484  cdlemk11  41485  cdlemk12  41486  cdlemkole  41489  cdlemk14  41490  cdlemk15  41491  cdlemk16a  41492  cdlemk16  41493  cdlemk18  41504  cdlemk19  41505  cdlemk7u  41506  cdlemk11u  41507  cdlemk12u  41508  cdlemk21N  41509  cdlemk20  41510  cdlemkoatnle-2N  41511  cdlemk13-2N  41512  cdlemkole-2N  41513  cdlemk14-2N  41514  cdlemk15-2N  41515  cdlemk16-2N  41516  cdlemk17-2N  41517  cdlemk18-2N  41522  cdlemk19-2N  41523  cdlemk7u-2N  41524  cdlemk11u-2N  41525  cdlemk12u-2N  41526  cdlemk21-2N  41527  cdlemk20-2N  41528  cdlemk22  41529  cdlemk27-3  41543  cdlemk33N  41545  cdlemk11ta  41565  cdlemkid3N  41569  cdlemk11tc  41581  cdlemk11t  41582  cdlemk45  41583  cdlemk46  41584  cdlemk47  41585  cdlemk48  41586  cdlemk49  41587  cdlemk50  41588  cdlemk51  41589  cdlemk52  41590  cdlemk53a  41591  cdlemk55b  41596  cdlemkyyN  41598  cdlemk55u1  41601  cdlemk39u1  41603  cdlemk56  41607  cdlemm10N  41754  dihord1  41854  dihord2a  41855  dihord2b  41856  dihord10  41859  dihord4  41894  dihord5apre  41898  dihglblem2N  41930  dihjatc1  41947  dihjatc2N  41948  dihjatc3  41949  dihmeetlem15N  41957  dihmeetlem20N  41962  mapdpglem24  42340  hdmap14lem11  42514  hdmap14lem12  42515  flt4lem5  43244  mzpsubst  43341  monotuz  43530  congmul  43556  congsub  43559  ntrclsiso  44655  ntrclskb  44657  ntrclsk3  44658  infleinf  45945  mullimc  46190  mullimcf  46197  0ellimcdiv  46221  limclner  46223  sge0xaddlem2  47006  isubgr3stgrlem3  48588  lincdifsn  49055  itschlc0yqe  49391  itscnhlc0xyqsol  49396  itsclc0xyqsolr  49400  itsclquadeu  49408