Theorem simp12 1205

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  simp112  1304  simp212  1313  simp312  1322  dvdsgcd  16486  coprimeprodsq  16741  pythagtriplem4  16752  pythagtriplem13  16760  pythagtriplem14  16761  pythagtriplem16  16763  pythagtrip  16767  pceu  16779  mremre  17548  lsmpropd  19545  m2cpminvid  22255  decpmatid  22272  mply1topmatcllem  22305  cmpsublem  22903  isfil2  23360  cxple2a  26207  isosctr  26326  nolesgn2o  27174  nolesgn2ores  27175  nogesgn1o  27176  nogesgn1ores  27177  nolt02o  27198  nogt01o  27199  sslttr  27309  cofsslt  27407  coinitsslt  27408  cofcut2  27411  brbtwn2  28194  colinearalg  28199  ax5seg  28227  axcontlem4  28256  bayesth  33469  bnj1204  34054  bnj1279  34060  ofscom  35010  btwndiff  35030  ifscgr  35047  brofs2  35080  brifs2  35081  fscgr  35083  btwnconn1lem1  35090  btwnconn1lem2  35091  btwnconn1lem3  35092  btwnconn1lem4  35093  btwnconn1lem12  35101  seglecgr12im  35113  seglecgr12  35114  ivthALT  35268  islshpcv  37971  lkrshp  38023  lshpsmreu  38027  lshpkrlem5  38032  cvrval3  38332  4noncolr3  38372  4noncolr2  38373  4noncolr1  38374  athgt  38375  3dimlem2  38378  3dimlem3a  38379  3dimlem4a  38382  3dimlem4  38383  3dimlem4OLDN  38384  1cvratex  38392  hlatexch4  38400  ps-2b  38401  3atlem4  38405  llnnleat  38432  2atm  38446  ps-2c  38447  llnmlplnN  38458  lplnnlelln  38462  2atmat  38480  lvoli2  38500  lvolnlelln  38503  4atlem3b  38517  4atlem10  38525  4atlem11a  38526  4atlem11b  38527  4atlem12a  38529  lplncvrlvol2  38534  2lplnja  38538  dalemswapyz  38575  lneq2at  38697  2lnat  38703  cdlema1N  38710  cdlemb  38713  paddasslem15  38753  pmodlem1  38765  llnmod2i2  38782  llnexchb2lem  38787  dalawlem1  38790  dalawlem3  38792  dalawlem4  38793  dalawlem6  38795  dalawlem7  38796  dalawlem9  38798  dalawlem10  38799  dalawlem11  38800  dalawlem12  38801  dalawlem13  38802  dalawlem15  38804  osumcllem5N  38879  osumcllem6N  38880  osumcllem7N  38881  osumcllem9N  38883  osumcllem10N  38884  osumcllem11N  38885  pl42lem1N  38898  lhpmcvr5N  38946  lhp2atne  38953  lhp2at0ne  38955  4atexlempw  38968  4atexlemex6  38993  4atexlem7  38994  ldilco  39035  ltrneq  39068  trlval2  39082  trlnidat  39092  cdlemd7  39123  cdleme7aa  39161  cdleme7c  39164  cdleme7d  39165  cdleme7e  39166  cdleme7ga  39167  cdleme7  39168  cdleme11c  39180  cdleme11e  39182  cdleme11l  39188  cdleme11  39189  cdleme14  39192  cdleme15a  39193  cdleme15c  39195  cdleme16b  39198  cdleme16c  39199  cdleme16d  39200  cdleme16e  39201  cdleme16f  39202  cdleme0nex  39209  cdleme18d  39214  cdleme19b  39223  cdleme19d  39225  cdleme19e  39226  cdleme20f  39233  cdleme20k  39238  cdleme20l1  39239  cdleme20l2  39240  cdleme20l  39241  cdleme20m  39242  cdleme21a  39244  cdleme21b  39245  cdleme21ct  39248  cdleme21d  39249  cdleme21e  39250  cdleme21f  39251  cdleme21h  39253  cdleme21i  39254  cdleme22eALTN  39264  cdleme22f2  39266  cdleme22g  39267  cdleme24  39271  cdleme25a  39272  cdleme25c  39274  cdleme25dN  39275  cdleme26e  39278  cdleme26ee  39279  cdleme26eALTN  39280  cdleme27N  39288  cdleme28a  39289  cdleme28b  39290  cdleme28  39292  cdlemefr32sn2aw  39323  cdlemefs32sn1aw  39333  cdleme43fsv1snlem  39339  cdleme41sn3a  39352  cdleme32c  39362  cdleme32e  39364  cdleme32le  39366  cdleme35a  39367  cdleme35b  39369  cdleme35c  39370  cdleme35e  39372  cdleme35f  39373  cdleme36a  39379  cdleme36m  39380  cdleme39a  39384  cdleme40m  39386  cdleme40n  39387  cdleme43bN  39409  cdleme43dN  39411  cdleme46f2g2  39412  cdleme46f2g1  39413  cdleme17d2  39414  cdleme4gfv  39426  cdlemeg49le  39430  cdlemeg46c  39432  cdlemeg46fvaw  39435  cdlemeg46nlpq  39436  cdlemeg46gfre  39451  cdleme50trn2  39470  cdleme  39479  cdlemg2idN  39515  cdlemg7fvbwN  39526  cdlemg10bALTN  39555  cdlemg10a  39559  cdlemg12d  39565  cdlemg12g  39568  cdlemg12  39569  cdlemg13a  39570  cdlemg13  39571  cdlemg17b  39581  cdlemg17dN  39582  cdlemg17dALTN  39583  cdlemg17e  39584  cdlemg17f  39585  cdlemg17i  39588  cdlemg17pq  39591  cdlemg17bq  39592  cdlemg17iqN  39593  cdlemg18d  39600  cdlemg18  39601  cdlemg19a  39602  cdlemg19  39603  cdlemg21  39605  cdlemg27a  39611  cdlemg28a  39612  cdlemg31b0N  39613  cdlemg27b  39615  cdlemg31c  39618  cdlemg33b0  39620  cdlemg33c0  39621  cdlemg28  39623  cdlemg33a  39625  cdlemg33  39630  cdlemg36  39633  ltrnco  39638  cdlemg44  39652  cdlemg47  39655  tendococl  39691  tendoplcl  39700  cdlemh1  39734  cdlemh2  39735  cdlemh  39736  cdlemi  39739  tendocan  39743  cdlemk5  39755  cdlemk6  39756  cdlemk7  39767  cdlemk11  39768  cdlemk12  39769  cdlemkole  39772  cdlemk14  39773  cdlemk15  39774  cdlemk16a  39775  cdlemk16  39776  cdlemk18  39787  cdlemk19  39788  cdlemk7u  39789  cdlemk11u  39790  cdlemk12u  39791  cdlemk21N  39792  cdlemk20  39793  cdlemkoatnle-2N  39794  cdlemk13-2N  39795  cdlemkole-2N  39796  cdlemk14-2N  39797  cdlemk15-2N  39798  cdlemk16-2N  39799  cdlemk17-2N  39800  cdlemk18-2N  39805  cdlemk19-2N  39806  cdlemk7u-2N  39807  cdlemk11u-2N  39808  cdlemk12u-2N  39809  cdlemk21-2N  39810  cdlemk20-2N  39811  cdlemk22  39812  cdlemk27-3  39826  cdlemk33N  39828  cdlemk11ta  39848  cdlemkid3N  39852  cdlemk11tc  39864  cdlemk11t  39865  cdlemk45  39866  cdlemk46  39867  cdlemk47  39868  cdlemk48  39869  cdlemk49  39870  cdlemk50  39871  cdlemk51  39872  cdlemk52  39873  cdlemk53a  39874  cdlemk55b  39879  cdlemkyyN  39881  cdlemk55u1  39884  cdlemk39u1  39886  cdlemk56  39890  cdlemm10N  40037  dihord1  40137  dihord2a  40138  dihord2b  40139  dihord10  40142  dihord4  40177  dihord5apre  40181  dihglblem2N  40213  dihjatc1  40230  dihjatc2N  40231  dihjatc3  40232  dihmeetlem15N  40240  dihmeetlem20N  40245  mapdpglem24  40623  hdmap14lem11  40797  hdmap14lem12  40798  flt4lem5  41440  mzpsubst  41534  monotuz  41728  congmul  41754  congsub  41757  ntrclsiso  42866  ntrclskb  42868  ntrclsk3  42869  infleinf  44130  mullimc  44380  mullimcf  44387  0ellimcdiv  44413  limclner  44415  sge0xaddlem2  45198  lincdifsn  47153  itschlc0yqe  47494  itscnhlc0xyqsol  47499  itsclc0xyqsolr  47503  itsclquadeu  47511