Theorem simp12 1200

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp112  1299  simp212  1308  simp312  1317  dvdsgcd  15886  coprimeprodsq  16139  pythagtriplem4  16150  pythagtriplem13  16158  pythagtriplem14  16159  pythagtriplem16  16161  pythagtrip  16165  pceu  16177  mremre  16869  lsmpropd  18797  m2cpminvid  21355  decpmatid  21372  mply1topmatcllem  21405  cmpsublem  22001  isfil2  22458  cxple2a  25276  isosctr  25393  brbtwn2  26685  colinearalg  26690  ax5seg  26718  axcontlem4  26747  bayesth  31692  bnj1204  32279  bnj1279  32285  nolesgn2o  33173  nolesgn2ores  33174  nolt02o  33194  ofscom  33463  btwndiff  33483  ifscgr  33500  brofs2  33533  brifs2  33534  fscgr  33536  btwnconn1lem1  33543  btwnconn1lem2  33544  btwnconn1lem3  33545  btwnconn1lem4  33546  btwnconn1lem12  33554  seglecgr12im  33566  seglecgr12  33567  ivthALT  33678  islshpcv  36183  lkrshp  36235  lshpsmreu  36239  lshpkrlem5  36244  cvrval3  36543  4noncolr3  36583  4noncolr2  36584  4noncolr1  36585  athgt  36586  3dimlem2  36589  3dimlem3a  36590  3dimlem4a  36593  3dimlem4  36594  3dimlem4OLDN  36595  1cvratex  36603  hlatexch4  36611  ps-2b  36612  3atlem4  36616  llnnleat  36643  2atm  36657  ps-2c  36658  llnmlplnN  36669  lplnnlelln  36673  2atmat  36691  lvoli2  36711  lvolnlelln  36714  4atlem3b  36728  4atlem10  36736  4atlem11a  36737  4atlem11b  36738  4atlem12a  36740  lplncvrlvol2  36745  2lplnja  36749  dalemswapyz  36786  lneq2at  36908  2lnat  36914  cdlema1N  36921  cdlemb  36924  paddasslem15  36964  pmodlem1  36976  llnmod2i2  36993  llnexchb2lem  36998  dalawlem1  37001  dalawlem3  37003  dalawlem4  37004  dalawlem6  37006  dalawlem7  37007  dalawlem9  37009  dalawlem10  37010  dalawlem11  37011  dalawlem12  37012  dalawlem13  37013  dalawlem15  37015  osumcllem5N  37090  osumcllem6N  37091  osumcllem7N  37092  osumcllem9N  37094  osumcllem10N  37095  osumcllem11N  37096  pl42lem1N  37109  lhpmcvr5N  37157  lhp2atne  37164  lhp2at0ne  37166  4atexlempw  37179  4atexlemex6  37204  4atexlem7  37205  ldilco  37246  ltrneq  37279  trlval2  37293  trlnidat  37303  cdlemd7  37334  cdleme7aa  37372  cdleme7c  37375  cdleme7d  37376  cdleme7e  37377  cdleme7ga  37378  cdleme7  37379  cdleme11c  37391  cdleme11e  37393  cdleme11l  37399  cdleme11  37400  cdleme14  37403  cdleme15a  37404  cdleme15c  37406  cdleme16b  37409  cdleme16c  37410  cdleme16d  37411  cdleme16e  37412  cdleme16f  37413  cdleme0nex  37420  cdleme18d  37425  cdleme19b  37434  cdleme19d  37436  cdleme19e  37437  cdleme20f  37444  cdleme20k  37449  cdleme20l1  37450  cdleme20l2  37451  cdleme20l  37452  cdleme20m  37453  cdleme21a  37455  cdleme21b  37456  cdleme21ct  37459  cdleme21d  37460  cdleme21e  37461  cdleme21f  37462  cdleme21h  37464  cdleme21i  37465  cdleme22eALTN  37475  cdleme22f2  37477  cdleme22g  37478  cdleme24  37482  cdleme25a  37483  cdleme25c  37485  cdleme25dN  37486  cdleme26e  37489  cdleme26ee  37490  cdleme26eALTN  37491  cdleme27N  37499  cdleme28a  37500  cdleme28b  37501  cdleme28  37503  cdlemefr32sn2aw  37534  cdlemefs32sn1aw  37544  cdleme43fsv1snlem  37550  cdleme41sn3a  37563  cdleme32c  37573  cdleme32e  37575  cdleme32le  37577  cdleme35a  37578  cdleme35b  37580  cdleme35c  37581  cdleme35e  37583  cdleme35f  37584  cdleme36a  37590  cdleme36m  37591  cdleme39a  37595  cdleme40m  37597  cdleme40n  37598  cdleme43bN  37620  cdleme43dN  37622  cdleme46f2g2  37623  cdleme46f2g1  37624  cdleme17d2  37625  cdleme4gfv  37637  cdlemeg49le  37641  cdlemeg46c  37643  cdlemeg46fvaw  37646  cdlemeg46nlpq  37647  cdlemeg46gfre  37662  cdleme50trn2  37681  cdleme  37690  cdlemg2idN  37726  cdlemg7fvbwN  37737  cdlemg10bALTN  37766  cdlemg10a  37770  cdlemg12d  37776  cdlemg12g  37779  cdlemg12  37780  cdlemg13a  37781  cdlemg13  37782  cdlemg17b  37792  cdlemg17dN  37793  cdlemg17dALTN  37794  cdlemg17e  37795  cdlemg17f  37796  cdlemg17i  37799  cdlemg17pq  37802  cdlemg17bq  37803  cdlemg17iqN  37804  cdlemg18d  37811  cdlemg18  37812  cdlemg19a  37813  cdlemg19  37814  cdlemg21  37816  cdlemg27a  37822  cdlemg28a  37823  cdlemg31b0N  37824  cdlemg27b  37826  cdlemg31c  37829  cdlemg33b0  37831  cdlemg33c0  37832  cdlemg28  37834  cdlemg33a  37836  cdlemg33  37841  cdlemg36  37844  ltrnco  37849  cdlemg44  37863  cdlemg47  37866  tendococl  37902  tendoplcl  37911  cdlemh1  37945  cdlemh2  37946  cdlemh  37947  cdlemi  37950  tendocan  37954  cdlemk5  37966  cdlemk6  37967  cdlemk7  37978  cdlemk11  37979  cdlemk12  37980  cdlemkole  37983  cdlemk14  37984  cdlemk15  37985  cdlemk16a  37986  cdlemk16  37987  cdlemk18  37998  cdlemk19  37999  cdlemk7u  38000  cdlemk11u  38001  cdlemk12u  38002  cdlemk21N  38003  cdlemk20  38004  cdlemkoatnle-2N  38005  cdlemk13-2N  38006  cdlemkole-2N  38007  cdlemk14-2N  38008  cdlemk15-2N  38009  cdlemk16-2N  38010  cdlemk17-2N  38011  cdlemk18-2N  38016  cdlemk19-2N  38017  cdlemk7u-2N  38018  cdlemk11u-2N  38019  cdlemk12u-2N  38020  cdlemk21-2N  38021  cdlemk20-2N  38022  cdlemk22  38023  cdlemk27-3  38037  cdlemk33N  38039  cdlemk11ta  38059  cdlemkid3N  38063  cdlemk11tc  38075  cdlemk11t  38076  cdlemk45  38077  cdlemk46  38078  cdlemk47  38079  cdlemk48  38080  cdlemk49  38081  cdlemk50  38082  cdlemk51  38083  cdlemk52  38084  cdlemk53a  38085  cdlemk55b  38090  cdlemkyyN  38092  cdlemk55u1  38095  cdlemk39u1  38097  cdlemk56  38101  cdlemm10N  38248  dihord1  38348  dihord2a  38349  dihord2b  38350  dihord10  38353  dihord4  38388  dihord5apre  38392  dihglblem2N  38424  dihjatc1  38441  dihjatc2N  38442  dihjatc3  38443  dihmeetlem15N  38451  dihmeetlem20N  38456  mapdpglem24  38834  hdmap14lem11  39008  hdmap14lem12  39009  mzpsubst  39338  monotuz  39531  congmul  39557  congsub  39560  ntrclsiso  40410  ntrclskb  40412  ntrclsk3  40413  infleinf  41633  mullimc  41890  mullimcf  41897  0ellimcdiv  41923  limclner  41925  sge0xaddlem2  42710  lincdifsn  44473  itschlc0yqe  44741  itscnhlc0xyqsol  44746  itsclc0xyqsolr  44750  itsclquadeu  44758