Theorem simp12 1201

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  simp112  1300  simp212  1309  simp312  1318  dvdsgcd  15882  coprimeprodsq  16135  pythagtriplem4  16146  pythagtriplem13  16154  pythagtriplem14  16155  pythagtriplem16  16157  pythagtrip  16161  pceu  16173  mremre  16867  lsmpropd  18795  m2cpminvid  21358  decpmatid  21375  mply1topmatcllem  21408  cmpsublem  22004  isfil2  22461  cxple2a  25290  isosctr  25407  brbtwn2  26699  colinearalg  26704  ax5seg  26732  axcontlem4  26761  bayesth  31807  bnj1204  32394  bnj1279  32400  nolesgn2o  33291  nolesgn2ores  33292  nolt02o  33312  ofscom  33581  btwndiff  33601  ifscgr  33618  brofs2  33651  brifs2  33652  fscgr  33654  btwnconn1lem1  33661  btwnconn1lem2  33662  btwnconn1lem3  33663  btwnconn1lem4  33664  btwnconn1lem12  33672  seglecgr12im  33684  seglecgr12  33685  ivthALT  33796  islshpcv  36349  lkrshp  36401  lshpsmreu  36405  lshpkrlem5  36410  cvrval3  36709  4noncolr3  36749  4noncolr2  36750  4noncolr1  36751  athgt  36752  3dimlem2  36755  3dimlem3a  36756  3dimlem4a  36759  3dimlem4  36760  3dimlem4OLDN  36761  1cvratex  36769  hlatexch4  36777  ps-2b  36778  3atlem4  36782  llnnleat  36809  2atm  36823  ps-2c  36824  llnmlplnN  36835  lplnnlelln  36839  2atmat  36857  lvoli2  36877  lvolnlelln  36880  4atlem3b  36894  4atlem10  36902  4atlem11a  36903  4atlem11b  36904  4atlem12a  36906  lplncvrlvol2  36911  2lplnja  36915  dalemswapyz  36952  lneq2at  37074  2lnat  37080  cdlema1N  37087  cdlemb  37090  paddasslem15  37130  pmodlem1  37142  llnmod2i2  37159  llnexchb2lem  37164  dalawlem1  37167  dalawlem3  37169  dalawlem4  37170  dalawlem6  37172  dalawlem7  37173  dalawlem9  37175  dalawlem10  37176  dalawlem11  37177  dalawlem12  37178  dalawlem13  37179  dalawlem15  37181  osumcllem5N  37256  osumcllem6N  37257  osumcllem7N  37258  osumcllem9N  37260  osumcllem10N  37261  osumcllem11N  37262  pl42lem1N  37275  lhpmcvr5N  37323  lhp2atne  37330  lhp2at0ne  37332  4atexlempw  37345  4atexlemex6  37370  4atexlem7  37371  ldilco  37412  ltrneq  37445  trlval2  37459  trlnidat  37469  cdlemd7  37500  cdleme7aa  37538  cdleme7c  37541  cdleme7d  37542  cdleme7e  37543  cdleme7ga  37544  cdleme7  37545  cdleme11c  37557  cdleme11e  37559  cdleme11l  37565  cdleme11  37566  cdleme14  37569  cdleme15a  37570  cdleme15c  37572  cdleme16b  37575  cdleme16c  37576  cdleme16d  37577  cdleme16e  37578  cdleme16f  37579  cdleme0nex  37586  cdleme18d  37591  cdleme19b  37600  cdleme19d  37602  cdleme19e  37603  cdleme20f  37610  cdleme20k  37615  cdleme20l1  37616  cdleme20l2  37617  cdleme20l  37618  cdleme20m  37619  cdleme21a  37621  cdleme21b  37622  cdleme21ct  37625  cdleme21d  37626  cdleme21e  37627  cdleme21f  37628  cdleme21h  37630  cdleme21i  37631  cdleme22eALTN  37641  cdleme22f2  37643  cdleme22g  37644  cdleme24  37648  cdleme25a  37649  cdleme25c  37651  cdleme25dN  37652  cdleme26e  37655  cdleme26ee  37656  cdleme26eALTN  37657  cdleme27N  37665  cdleme28a  37666  cdleme28b  37667  cdleme28  37669  cdlemefr32sn2aw  37700  cdlemefs32sn1aw  37710  cdleme43fsv1snlem  37716  cdleme41sn3a  37729  cdleme32c  37739  cdleme32e  37741  cdleme32le  37743  cdleme35a  37744  cdleme35b  37746  cdleme35c  37747  cdleme35e  37749  cdleme35f  37750  cdleme36a  37756  cdleme36m  37757  cdleme39a  37761  cdleme40m  37763  cdleme40n  37764  cdleme43bN  37786  cdleme43dN  37788  cdleme46f2g2  37789  cdleme46f2g1  37790  cdleme17d2  37791  cdleme4gfv  37803  cdlemeg49le  37807  cdlemeg46c  37809  cdlemeg46fvaw  37812  cdlemeg46nlpq  37813  cdlemeg46gfre  37828  cdleme50trn2  37847  cdleme  37856  cdlemg2idN  37892  cdlemg7fvbwN  37903  cdlemg10bALTN  37932  cdlemg10a  37936  cdlemg12d  37942  cdlemg12g  37945  cdlemg12  37946  cdlemg13a  37947  cdlemg13  37948  cdlemg17b  37958  cdlemg17dN  37959  cdlemg17dALTN  37960  cdlemg17e  37961  cdlemg17f  37962  cdlemg17i  37965  cdlemg17pq  37968  cdlemg17bq  37969  cdlemg17iqN  37970  cdlemg18d  37977  cdlemg18  37978  cdlemg19a  37979  cdlemg19  37980  cdlemg21  37982  cdlemg27a  37988  cdlemg28a  37989  cdlemg31b0N  37990  cdlemg27b  37992  cdlemg31c  37995  cdlemg33b0  37997  cdlemg33c0  37998  cdlemg28  38000  cdlemg33a  38002  cdlemg33  38007  cdlemg36  38010  ltrnco  38015  cdlemg44  38029  cdlemg47  38032  tendococl  38068  tendoplcl  38077  cdlemh1  38111  cdlemh2  38112  cdlemh  38113  cdlemi  38116  tendocan  38120  cdlemk5  38132  cdlemk6  38133  cdlemk7  38144  cdlemk11  38145  cdlemk12  38146  cdlemkole  38149  cdlemk14  38150  cdlemk15  38151  cdlemk16a  38152  cdlemk16  38153  cdlemk18  38164  cdlemk19  38165  cdlemk7u  38166  cdlemk11u  38167  cdlemk12u  38168  cdlemk21N  38169  cdlemk20  38170  cdlemkoatnle-2N  38171  cdlemk13-2N  38172  cdlemkole-2N  38173  cdlemk14-2N  38174  cdlemk15-2N  38175  cdlemk16-2N  38176  cdlemk17-2N  38177  cdlemk18-2N  38182  cdlemk19-2N  38183  cdlemk7u-2N  38184  cdlemk11u-2N  38185  cdlemk12u-2N  38186  cdlemk21-2N  38187  cdlemk20-2N  38188  cdlemk22  38189  cdlemk27-3  38203  cdlemk33N  38205  cdlemk11ta  38225  cdlemkid3N  38229  cdlemk11tc  38241  cdlemk11t  38242  cdlemk45  38243  cdlemk46  38244  cdlemk47  38245  cdlemk48  38246  cdlemk49  38247  cdlemk50  38248  cdlemk51  38249  cdlemk52  38250  cdlemk53a  38251  cdlemk55b  38256  cdlemkyyN  38258  cdlemk55u1  38261  cdlemk39u1  38263  cdlemk56  38267  cdlemm10N  38414  dihord1  38514  dihord2a  38515  dihord2b  38516  dihord10  38519  dihord4  38554  dihord5apre  38558  dihglblem2N  38590  dihjatc1  38607  dihjatc2N  38608  dihjatc3  38609  dihmeetlem15N  38617  dihmeetlem20N  38622  mapdpglem24  39000  hdmap14lem11  39174  hdmap14lem12  39175  mzpsubst  39689  monotuz  39882  congmul  39908  congsub  39911  ntrclsiso  40770  ntrclskb  40772  ntrclsk3  40773  infleinf  42004  mullimc  42258  mullimcf  42265  0ellimcdiv  42291  limclner  42293  sge0xaddlem2  43073  lincdifsn  44833  itschlc0yqe  45174  itscnhlc0xyqsol  45179  itsclc0xyqsolr  45183  itsclquadeu  45191