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  16722  coprimeprodsq  16991  pythagtriplem4  17002  pythagtriplem13  17010  pythagtriplem14  17011  pythagtriplem16  17013  pythagtrip  17017  pceu  17029  mremre  17779  lsmpropd  19896  m2cpminvid  23076  decpmatid  23093  mply1topmatcllem  23126  cmpsublem  23722  isfil2  24180  cxple2a  27032  isosctr  27154  flt4lem5  27985  nolesgn2o  28033  nolesgn2ores  28034  nogesgn1o  28035  nogesgn1ores  28036  nolt02o  28057  nogt01o  28058  sltstr  28178  cofslts  28309  coinitslts  28310  cofcut2  28313  onsfi  28747  brbtwn2  29488  colinearalg  29493  ax5seg  29521  axcontlem4  29550  bayesth  35117  bnj1204  35688  bnj1279  35694  ofscom  36864  btwndiff  36884  ifscgr  36901  brofs2  36934  brifs2  36935  fscgr  36937  btwnconn1lem1  36944  btwnconn1lem2  36945  btwnconn1lem3  36946  btwnconn1lem4  36947  btwnconn1lem12  36955  seglecgr12im  36967  seglecgr12  36968  ivthALT  37215  islshpcv  40203  lkrshp  40255  lshpsmreu  40259  lshpkrlem5  40264  cvrval3  40563  4noncolr3  40603  4noncolr2  40604  4noncolr1  40605  athgt  40606  3dimlem2  40609  3dimlem3a  40610  3dimlem4a  40613  3dimlem4  40614  3dimlem4OLDN  40615  1cvratex  40623  hlatexch4  40631  ps-2b  40632  3atlem4  40636  llnnleat  40663  2atm  40677  ps-2c  40678  llnmlplnN  40689  lplnnlelln  40693  2atmat  40711  lvoli2  40731  lvolnlelln  40734  4atlem3b  40748  4atlem10  40756  4atlem11a  40757  4atlem11b  40758  4atlem12a  40760  lplncvrlvol2  40765  2lplnja  40769  dalemswapyz  40806  lneq2at  40928  2lnat  40934  cdlema1N  40941  cdlemb  40944  paddasslem15  40984  pmodlem1  40996  llnmod2i2  41013  llnexchb2lem  41018  dalawlem1  41021  dalawlem3  41023  dalawlem4  41024  dalawlem6  41026  dalawlem7  41027  dalawlem9  41029  dalawlem10  41030  dalawlem11  41031  dalawlem12  41032  dalawlem13  41033  dalawlem15  41035  osumcllem5N  41110  osumcllem6N  41111  osumcllem7N  41112  osumcllem9N  41114  osumcllem10N  41115  osumcllem11N  41116  pl42lem1N  41129  lhpmcvr5N  41177  lhp2atne  41184  lhp2at0ne  41186  4atexlempw  41199  4atexlemex6  41224  4atexlem7  41225  ldilco  41266  ltrneq  41299  trlval2  41313  trlnidat  41323  cdlemd7  41354  cdleme7aa  41392  cdleme7c  41395  cdleme7d  41396  cdleme7e  41397  cdleme7ga  41398  cdleme7  41399  cdleme11c  41411  cdleme11e  41413  cdleme11l  41419  cdleme11  41420  cdleme14  41423  cdleme15a  41424  cdleme15c  41426  cdleme16b  41429  cdleme16c  41430  cdleme16d  41431  cdleme16e  41432  cdleme16f  41433  cdleme0nex  41440  cdleme18d  41445  cdleme19b  41454  cdleme19d  41456  cdleme19e  41457  cdleme20f  41464  cdleme20k  41469  cdleme20l1  41470  cdleme20l2  41471  cdleme20l  41472  cdleme20m  41473  cdleme21a  41475  cdleme21b  41476  cdleme21ct  41479  cdleme21d  41480  cdleme21e  41481  cdleme21f  41482  cdleme21h  41484  cdleme21i  41485  cdleme22eALTN  41495  cdleme22f2  41497  cdleme22g  41498  cdleme24  41502  cdleme25a  41503  cdleme25c  41505  cdleme25dN  41506  cdleme26e  41509  cdleme26ee  41510  cdleme26eALTN  41511  cdleme27N  41519  cdleme28a  41520  cdleme28b  41521  cdleme28  41523  cdlemefr32sn2aw  41554  cdlemefs32sn1aw  41564  cdleme43fsv1snlem  41570  cdleme41sn3a  41583  cdleme32c  41593  cdleme32e  41595  cdleme32le  41597  cdleme35a  41598  cdleme35b  41600  cdleme35c  41601  cdleme35e  41603  cdleme35f  41604  cdleme36a  41610  cdleme36m  41611  cdleme39a  41615  cdleme40m  41617  cdleme40n  41618  cdleme43bN  41640  cdleme43dN  41642  cdleme46f2g2  41643  cdleme46f2g1  41644  cdleme17d2  41645  cdleme4gfv  41657  cdlemeg49le  41661  cdlemeg46c  41663  cdlemeg46fvaw  41666  cdlemeg46nlpq  41667  cdlemeg46gfre  41682  cdleme50trn2  41701  cdleme  41710  cdlemg2idN  41746  cdlemg7fvbwN  41757  cdlemg10bALTN  41786  cdlemg10a  41790  cdlemg12d  41796  cdlemg12g  41799  cdlemg12  41800  cdlemg13a  41801  cdlemg13  41802  cdlemg17b  41812  cdlemg17dN  41813  cdlemg17dALTN  41814  cdlemg17e  41815  cdlemg17f  41816  cdlemg17i  41819  cdlemg17pq  41822  cdlemg17bq  41823  cdlemg17iqN  41824  cdlemg18d  41831  cdlemg18  41832  cdlemg19a  41833  cdlemg19  41834  cdlemg21  41836  cdlemg27a  41842  cdlemg28a  41843  cdlemg31b0N  41844  cdlemg27b  41846  cdlemg31c  41849  cdlemg33b0  41851  cdlemg33c0  41852  cdlemg28  41854  cdlemg33a  41856  cdlemg33  41861  cdlemg36  41864  ltrnco  41869  cdlemg44  41883  cdlemg47  41886  tendococl  41922  tendoplcl  41931  cdlemh1  41965  cdlemh2  41966  cdlemh  41967  cdlemi  41970  tendocan  41974  cdlemk5  41986  cdlemk6  41987  cdlemk7  41998  cdlemk11  41999  cdlemk12  42000  cdlemkole  42003  cdlemk14  42004  cdlemk15  42005  cdlemk16a  42006  cdlemk16  42007  cdlemk18  42018  cdlemk19  42019  cdlemk7u  42020  cdlemk11u  42021  cdlemk12u  42022  cdlemk21N  42023  cdlemk20  42024  cdlemkoatnle-2N  42025  cdlemk13-2N  42026  cdlemkole-2N  42027  cdlemk14-2N  42028  cdlemk15-2N  42029  cdlemk16-2N  42030  cdlemk17-2N  42031  cdlemk18-2N  42036  cdlemk19-2N  42037  cdlemk7u-2N  42038  cdlemk11u-2N  42039  cdlemk12u-2N  42040  cdlemk21-2N  42041  cdlemk20-2N  42042  cdlemk22  42043  cdlemk27-3  42057  cdlemk33N  42059  cdlemk11ta  42079  cdlemkid3N  42083  cdlemk11tc  42095  cdlemk11t  42096  cdlemk45  42097  cdlemk46  42098  cdlemk47  42099  cdlemk48  42100  cdlemk49  42101  cdlemk50  42102  cdlemk51  42103  cdlemk52  42104  cdlemk53a  42105  cdlemk55b  42110  cdlemkyyN  42112  cdlemk55u1  42115  cdlemk39u1  42117  cdlemk56  42121  cdlemm10N  42268  dihord1  42368  dihord2a  42369  dihord2b  42370  dihord10  42373  dihord4  42408  dihord5apre  42412  dihglblem2N  42444  dihjatc1  42461  dihjatc2N  42462  dihjatc3  42463  dihmeetlem15N  42471  dihmeetlem20N  42476  mapdpglem24  42854  hdmap14lem11  43028  hdmap14lem12  43029  mzpsubst  43852  monotuz  44041  congmul  44067  congsub  44070  ntrclsiso  45160  ntrclskb  45162  ntrclsk3  45163  infleinf  46476  mullimc  46721  mullimcf  46728  0ellimcdiv  46752  limclner  46754  sge0xaddlem2  47537  isubgr3stgrlem3  49159  lincdifsn  49629  itschlc0yqe  49965  itscnhlc0xyqsol  49970  itsclc0xyqsolr  49974  itsclquadeu  49982