Theorem simp12 1202

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp112  1301  simp212  1310  simp312  1319  dvdsgcd  16180  coprimeprodsq  16437  pythagtriplem4  16448  pythagtriplem13  16456  pythagtriplem14  16457  pythagtriplem16  16459  pythagtrip  16463  pceu  16475  mremre  17230  lsmpropd  19198  m2cpminvid  21810  decpmatid  21827  mply1topmatcllem  21860  cmpsublem  22458  isfil2  22915  cxple2a  25759  isosctr  25876  brbtwn2  27176  colinearalg  27181  ax5seg  27209  axcontlem4  27238  bayesth  32306  bnj1204  32892  bnj1279  32898  nolesgn2o  33801  nolesgn2ores  33802  nogesgn1o  33803  nogesgn1ores  33804  nolt02o  33825  nogt01o  33826  sslttr  33928  cofsslt  34015  coinitsslt  34016  cofcut2  34018  ofscom  34236  btwndiff  34256  ifscgr  34273  brofs2  34306  brifs2  34307  fscgr  34309  btwnconn1lem1  34316  btwnconn1lem2  34317  btwnconn1lem3  34318  btwnconn1lem4  34319  btwnconn1lem12  34327  seglecgr12im  34339  seglecgr12  34340  ivthALT  34451  islshpcv  36994  lkrshp  37046  lshpsmreu  37050  lshpkrlem5  37055  cvrval3  37354  4noncolr3  37394  4noncolr2  37395  4noncolr1  37396  athgt  37397  3dimlem2  37400  3dimlem3a  37401  3dimlem4a  37404  3dimlem4  37405  3dimlem4OLDN  37406  1cvratex  37414  hlatexch4  37422  ps-2b  37423  3atlem4  37427  llnnleat  37454  2atm  37468  ps-2c  37469  llnmlplnN  37480  lplnnlelln  37484  2atmat  37502  lvoli2  37522  lvolnlelln  37525  4atlem3b  37539  4atlem10  37547  4atlem11a  37548  4atlem11b  37549  4atlem12a  37551  lplncvrlvol2  37556  2lplnja  37560  dalemswapyz  37597  lneq2at  37719  2lnat  37725  cdlema1N  37732  cdlemb  37735  paddasslem15  37775  pmodlem1  37787  llnmod2i2  37804  llnexchb2lem  37809  dalawlem1  37812  dalawlem3  37814  dalawlem4  37815  dalawlem6  37817  dalawlem7  37818  dalawlem9  37820  dalawlem10  37821  dalawlem11  37822  dalawlem12  37823  dalawlem13  37824  dalawlem15  37826  osumcllem5N  37901  osumcllem6N  37902  osumcllem7N  37903  osumcllem9N  37905  osumcllem10N  37906  osumcllem11N  37907  pl42lem1N  37920  lhpmcvr5N  37968  lhp2atne  37975  lhp2at0ne  37977  4atexlempw  37990  4atexlemex6  38015  4atexlem7  38016  ldilco  38057  ltrneq  38090  trlval2  38104  trlnidat  38114  cdlemd7  38145  cdleme7aa  38183  cdleme7c  38186  cdleme7d  38187  cdleme7e  38188  cdleme7ga  38189  cdleme7  38190  cdleme11c  38202  cdleme11e  38204  cdleme11l  38210  cdleme11  38211  cdleme14  38214  cdleme15a  38215  cdleme15c  38217  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme16e  38223  cdleme16f  38224  cdleme0nex  38231  cdleme18d  38236  cdleme19b  38245  cdleme19d  38247  cdleme19e  38248  cdleme20f  38255  cdleme20k  38260  cdleme20l1  38261  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme21a  38266  cdleme21b  38267  cdleme21ct  38270  cdleme21d  38271  cdleme21e  38272  cdleme21f  38273  cdleme21h  38275  cdleme21i  38276  cdleme22eALTN  38286  cdleme22f2  38288  cdleme22g  38289  cdleme24  38293  cdleme25a  38294  cdleme25c  38296  cdleme25dN  38297  cdleme26e  38300  cdleme26ee  38301  cdleme26eALTN  38302  cdleme27N  38310  cdleme28a  38311  cdleme28b  38312  cdleme28  38314  cdlemefr32sn2aw  38345  cdlemefs32sn1aw  38355  cdleme43fsv1snlem  38361  cdleme41sn3a  38374  cdleme32c  38384  cdleme32e  38386  cdleme32le  38388  cdleme35a  38389  cdleme35b  38391  cdleme35c  38392  cdleme35e  38394  cdleme35f  38395  cdleme36a  38401  cdleme36m  38402  cdleme39a  38406  cdleme40m  38408  cdleme40n  38409  cdleme43bN  38431  cdleme43dN  38433  cdleme46f2g2  38434  cdleme46f2g1  38435  cdleme17d2  38436  cdleme4gfv  38448  cdlemeg49le  38452  cdlemeg46c  38454  cdlemeg46fvaw  38457  cdlemeg46nlpq  38458  cdlemeg46gfre  38473  cdleme50trn2  38492  cdleme  38501  cdlemg2idN  38537  cdlemg7fvbwN  38548  cdlemg10bALTN  38577  cdlemg10a  38581  cdlemg12d  38587  cdlemg12g  38590  cdlemg12  38591  cdlemg13a  38592  cdlemg13  38593  cdlemg17b  38603  cdlemg17dN  38604  cdlemg17dALTN  38605  cdlemg17e  38606  cdlemg17f  38607  cdlemg17i  38610  cdlemg17pq  38613  cdlemg17bq  38614  cdlemg17iqN  38615  cdlemg18d  38622  cdlemg18  38623  cdlemg19a  38624  cdlemg19  38625  cdlemg21  38627  cdlemg27a  38633  cdlemg28a  38634  cdlemg31b0N  38635  cdlemg27b  38637  cdlemg31c  38640  cdlemg33b0  38642  cdlemg33c0  38643  cdlemg28  38645  cdlemg33a  38647  cdlemg33  38652  cdlemg36  38655  ltrnco  38660  cdlemg44  38674  cdlemg47  38677  tendococl  38713  tendoplcl  38722  cdlemh1  38756  cdlemh2  38757  cdlemh  38758  cdlemi  38761  tendocan  38765  cdlemk5  38777  cdlemk6  38778  cdlemk7  38789  cdlemk11  38790  cdlemk12  38791  cdlemkole  38794  cdlemk14  38795  cdlemk15  38796  cdlemk16a  38797  cdlemk16  38798  cdlemk18  38809  cdlemk19  38810  cdlemk7u  38811  cdlemk11u  38812  cdlemk12u  38813  cdlemk21N  38814  cdlemk20  38815  cdlemkoatnle-2N  38816  cdlemk13-2N  38817  cdlemkole-2N  38818  cdlemk14-2N  38819  cdlemk15-2N  38820  cdlemk16-2N  38821  cdlemk17-2N  38822  cdlemk18-2N  38827  cdlemk19-2N  38828  cdlemk7u-2N  38829  cdlemk11u-2N  38830  cdlemk12u-2N  38831  cdlemk21-2N  38832  cdlemk20-2N  38833  cdlemk22  38834  cdlemk27-3  38848  cdlemk33N  38850  cdlemk11ta  38870  cdlemkid3N  38874  cdlemk11tc  38886  cdlemk11t  38887  cdlemk45  38888  cdlemk46  38889  cdlemk47  38890  cdlemk48  38891  cdlemk49  38892  cdlemk50  38893  cdlemk51  38894  cdlemk52  38895  cdlemk53a  38896  cdlemk55b  38901  cdlemkyyN  38903  cdlemk55u1  38906  cdlemk39u1  38908  cdlemk56  38912  cdlemm10N  39059  dihord1  39159  dihord2a  39160  dihord2b  39161  dihord10  39164  dihord4  39199  dihord5apre  39203  dihglblem2N  39235  dihjatc1  39252  dihjatc2N  39253  dihjatc3  39254  dihmeetlem15N  39262  dihmeetlem20N  39267  mapdpglem24  39645  hdmap14lem11  39819  hdmap14lem12  39820  flt4lem5  40403  mzpsubst  40486  monotuz  40679  congmul  40705  congsub  40708  ntrclsiso  41566  ntrclskb  41568  ntrclsk3  41569  infleinf  42801  mullimc  43047  mullimcf  43054  0ellimcdiv  43080  limclner  43082  sge0xaddlem2  43862  lincdifsn  45653  itschlc0yqe  45994  itscnhlc0xyqsol  45999  itsclc0xyqsolr  46003  itsclquadeu  46011