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 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ w3a 1103

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 1105

This theorem is referenced by:  simp112  1322  simp212  1331  simp312  1340  dvdsgcd  16603  coprimeprodsq  16869  pythagtriplem4  16880  pythagtriplem13  16888  pythagtriplem14  16889  pythagtriplem16  16891  pythagtrip  16895  pceu  16907  mremre  17657  lsmpropd  19748  m2cpminvid  22891  decpmatid  22908  mply1topmatcllem  22941  cmpsublem  23537  isfil2  23994  cxple2a  26842  isosctr  26964  nolesgn2o  27813  nolesgn2ores  27814  nogesgn1o  27815  nogesgn1ores  27816  nolt02o  27837  nogt01o  27838  sltstr  27958  cofslts  28089  coinitslts  28090  cofcut2  28093  onsfi  28527  brbtwn2  29233  colinearalg  29238  ax5seg  29266  axcontlem4  29295  bayesth  34807  bnj1204  35378  bnj1279  35384  ofscom  36477  btwndiff  36497  ifscgr  36514  brofs2  36547  brifs2  36548  fscgr  36550  btwnconn1lem1  36557  btwnconn1lem2  36558  btwnconn1lem3  36559  btwnconn1lem4  36560  btwnconn1lem12  36568  seglecgr12im  36580  seglecgr12  36581  ivthALT  36824  islshpcv  39805  lkrshp  39857  lshpsmreu  39861  lshpkrlem5  39866  cvrval3  40165  4noncolr3  40205  4noncolr2  40206  4noncolr1  40207  athgt  40208  3dimlem2  40211  3dimlem3a  40212  3dimlem4a  40215  3dimlem4  40216  3dimlem4OLDN  40217  1cvratex  40225  hlatexch4  40233  ps-2b  40234  3atlem4  40238  llnnleat  40265  2atm  40279  ps-2c  40280  llnmlplnN  40291  lplnnlelln  40295  2atmat  40313  lvoli2  40333  lvolnlelln  40336  4atlem3b  40350  4atlem10  40358  4atlem11a  40359  4atlem11b  40360  4atlem12a  40362  lplncvrlvol2  40367  2lplnja  40371  dalemswapyz  40408  lneq2at  40530  2lnat  40536  cdlema1N  40543  cdlemb  40546  paddasslem15  40586  pmodlem1  40598  llnmod2i2  40615  llnexchb2lem  40620  dalawlem1  40623  dalawlem3  40625  dalawlem4  40626  dalawlem6  40628  dalawlem7  40629  dalawlem9  40631  dalawlem10  40632  dalawlem11  40633  dalawlem12  40634  dalawlem13  40635  dalawlem15  40637  osumcllem5N  40712  osumcllem6N  40713  osumcllem7N  40714  osumcllem9N  40716  osumcllem10N  40717  osumcllem11N  40718  pl42lem1N  40731  lhpmcvr5N  40779  lhp2atne  40786  lhp2at0ne  40788  4atexlempw  40801  4atexlemex6  40826  4atexlem7  40827  ldilco  40868  ltrneq  40901  trlval2  40915  trlnidat  40925  cdlemd7  40956  cdleme7aa  40994  cdleme7c  40997  cdleme7d  40998  cdleme7e  40999  cdleme7ga  41000  cdleme7  41001  cdleme11c  41013  cdleme11e  41015  cdleme11l  41021  cdleme11  41022  cdleme14  41025  cdleme15a  41026  cdleme15c  41028  cdleme16b  41031  cdleme16c  41032  cdleme16d  41033  cdleme16e  41034  cdleme16f  41035  cdleme0nex  41042  cdleme18d  41047  cdleme19b  41056  cdleme19d  41058  cdleme19e  41059  cdleme20f  41066  cdleme20k  41071  cdleme20l1  41072  cdleme20l2  41073  cdleme20l  41074  cdleme20m  41075  cdleme21a  41077  cdleme21b  41078  cdleme21ct  41081  cdleme21d  41082  cdleme21e  41083  cdleme21f  41084  cdleme21h  41086  cdleme21i  41087  cdleme22eALTN  41097  cdleme22f2  41099  cdleme22g  41100  cdleme24  41104  cdleme25a  41105  cdleme25c  41107  cdleme25dN  41108  cdleme26e  41111  cdleme26ee  41112  cdleme26eALTN  41113  cdleme27N  41121  cdleme28a  41122  cdleme28b  41123  cdleme28  41125  cdlemefr32sn2aw  41156  cdlemefs32sn1aw  41166  cdleme43fsv1snlem  41172  cdleme41sn3a  41185  cdleme32c  41195  cdleme32e  41197  cdleme32le  41199  cdleme35a  41200  cdleme35b  41202  cdleme35c  41203  cdleme35e  41205  cdleme35f  41206  cdleme36a  41212  cdleme36m  41213  cdleme39a  41217  cdleme40m  41219  cdleme40n  41220  cdleme43bN  41242  cdleme43dN  41244  cdleme46f2g2  41245  cdleme46f2g1  41246  cdleme17d2  41247  cdleme4gfv  41259  cdlemeg49le  41263  cdlemeg46c  41265  cdlemeg46fvaw  41268  cdlemeg46nlpq  41269  cdlemeg46gfre  41284  cdleme50trn2  41303  cdleme  41312  cdlemg2idN  41348  cdlemg7fvbwN  41359  cdlemg10bALTN  41388  cdlemg10a  41392  cdlemg12d  41398  cdlemg12g  41401  cdlemg12  41402  cdlemg13a  41403  cdlemg13  41404  cdlemg17b  41414  cdlemg17dN  41415  cdlemg17dALTN  41416  cdlemg17e  41417  cdlemg17f  41418  cdlemg17i  41421  cdlemg17pq  41424  cdlemg17bq  41425  cdlemg17iqN  41426  cdlemg18d  41433  cdlemg18  41434  cdlemg19a  41435  cdlemg19  41436  cdlemg21  41438  cdlemg27a  41444  cdlemg28a  41445  cdlemg31b0N  41446  cdlemg27b  41448  cdlemg31c  41451  cdlemg33b0  41453  cdlemg33c0  41454  cdlemg28  41456  cdlemg33a  41458  cdlemg33  41463  cdlemg36  41466  ltrnco  41471  cdlemg44  41485  cdlemg47  41488  tendococl  41524  tendoplcl  41533  cdlemh1  41567  cdlemh2  41568  cdlemh  41569  cdlemi  41572  tendocan  41576  cdlemk5  41588  cdlemk6  41589  cdlemk7  41600  cdlemk11  41601  cdlemk12  41602  cdlemkole  41605  cdlemk14  41606  cdlemk15  41607  cdlemk16a  41608  cdlemk16  41609  cdlemk18  41620  cdlemk19  41621  cdlemk7u  41622  cdlemk11u  41623  cdlemk12u  41624  cdlemk21N  41625  cdlemk20  41626  cdlemkoatnle-2N  41627  cdlemk13-2N  41628  cdlemkole-2N  41629  cdlemk14-2N  41630  cdlemk15-2N  41631  cdlemk16-2N  41632  cdlemk17-2N  41633  cdlemk18-2N  41638  cdlemk19-2N  41639  cdlemk7u-2N  41640  cdlemk11u-2N  41641  cdlemk12u-2N  41642  cdlemk21-2N  41643  cdlemk20-2N  41644  cdlemk22  41645  cdlemk27-3  41659  cdlemk33N  41661  cdlemk11ta  41681  cdlemkid3N  41685  cdlemk11tc  41697  cdlemk11t  41698  cdlemk45  41699  cdlemk46  41700  cdlemk47  41701  cdlemk48  41702  cdlemk49  41703  cdlemk50  41704  cdlemk51  41705  cdlemk52  41706  cdlemk53a  41707  cdlemk55b  41712  cdlemkyyN  41714  cdlemk55u1  41717  cdlemk39u1  41719  cdlemk56  41723  cdlemm10N  41870  dihord1  41970  dihord2a  41971  dihord2b  41972  dihord10  41975  dihord4  42010  dihord5apre  42014  dihglblem2N  42046  dihjatc1  42063  dihjatc2N  42064  dihjatc3  42065  dihmeetlem15N  42073  dihmeetlem20N  42078  mapdpglem24  42456  hdmap14lem11  42630  hdmap14lem12  42631  flt4lem5  43362  mzpsubst  43459  monotuz  43648  congmul  43674  congsub  43677  ntrclsiso  44773  ntrclskb  44775  ntrclsk3  44776  infleinf  46067  mullimc  46312  mullimcf  46319  0ellimcdiv  46343  limclner  46345  sge0xaddlem2  47128  isubgr3stgrlem3  48710  lincdifsn  49181  itschlc0yqe  49517  itscnhlc0xyqsol  49522  itsclc0xyqsolr  49526  itsclquadeu  49534