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  15894  coprimeprodsq  16147  pythagtriplem4  16158  pythagtriplem13  16166  pythagtriplem14  16167  pythagtriplem16  16169  pythagtrip  16173  pceu  16185  mremre  16877  lsmpropd  18805  m2cpminvid  21363  decpmatid  21380  mply1topmatcllem  21413  cmpsublem  22009  isfil2  22466  cxple2a  25284  isosctr  25401  brbtwn2  26693  colinearalg  26698  ax5seg  26726  axcontlem4  26755  bayesth  31699  bnj1204  32286  bnj1279  32292  nolesgn2o  33180  nolesgn2ores  33181  nolt02o  33201  ofscom  33470  btwndiff  33490  ifscgr  33507  brofs2  33540  brifs2  33541  fscgr  33543  btwnconn1lem1  33550  btwnconn1lem2  33551  btwnconn1lem3  33552  btwnconn1lem4  33553  btwnconn1lem12  33561  seglecgr12im  33573  seglecgr12  33574  ivthALT  33685  islshpcv  36191  lkrshp  36243  lshpsmreu  36247  lshpkrlem5  36252  cvrval3  36551  4noncolr3  36591  4noncolr2  36592  4noncolr1  36593  athgt  36594  3dimlem2  36597  3dimlem3a  36598  3dimlem4a  36601  3dimlem4  36602  3dimlem4OLDN  36603  1cvratex  36611  hlatexch4  36619  ps-2b  36620  3atlem4  36624  llnnleat  36651  2atm  36665  ps-2c  36666  llnmlplnN  36677  lplnnlelln  36681  2atmat  36699  lvoli2  36719  lvolnlelln  36722  4atlem3b  36736  4atlem10  36744  4atlem11a  36745  4atlem11b  36746  4atlem12a  36748  lplncvrlvol2  36753  2lplnja  36757  dalemswapyz  36794  lneq2at  36916  2lnat  36922  cdlema1N  36929  cdlemb  36932  paddasslem15  36972  pmodlem1  36984  llnmod2i2  37001  llnexchb2lem  37006  dalawlem1  37009  dalawlem3  37011  dalawlem4  37012  dalawlem6  37014  dalawlem7  37015  dalawlem9  37017  dalawlem10  37018  dalawlem11  37019  dalawlem12  37020  dalawlem13  37021  dalawlem15  37023  osumcllem5N  37098  osumcllem6N  37099  osumcllem7N  37100  osumcllem9N  37102  osumcllem10N  37103  osumcllem11N  37104  pl42lem1N  37117  lhpmcvr5N  37165  lhp2atne  37172  lhp2at0ne  37174  4atexlempw  37187  4atexlemex6  37212  4atexlem7  37213  ldilco  37254  ltrneq  37287  trlval2  37301  trlnidat  37311  cdlemd7  37342  cdleme7aa  37380  cdleme7c  37383  cdleme7d  37384  cdleme7e  37385  cdleme7ga  37386  cdleme7  37387  cdleme11c  37399  cdleme11e  37401  cdleme11l  37407  cdleme11  37408  cdleme14  37411  cdleme15a  37412  cdleme15c  37414  cdleme16b  37417  cdleme16c  37418  cdleme16d  37419  cdleme16e  37420  cdleme16f  37421  cdleme0nex  37428  cdleme18d  37433  cdleme19b  37442  cdleme19d  37444  cdleme19e  37445  cdleme20f  37452  cdleme20k  37457  cdleme20l1  37458  cdleme20l2  37459  cdleme20l  37460  cdleme20m  37461  cdleme21a  37463  cdleme21b  37464  cdleme21ct  37467  cdleme21d  37468  cdleme21e  37469  cdleme21f  37470  cdleme21h  37472  cdleme21i  37473  cdleme22eALTN  37483  cdleme22f2  37485  cdleme22g  37486  cdleme24  37490  cdleme25a  37491  cdleme25c  37493  cdleme25dN  37494  cdleme26e  37497  cdleme26ee  37498  cdleme26eALTN  37499  cdleme27N  37507  cdleme28a  37508  cdleme28b  37509  cdleme28  37511  cdlemefr32sn2aw  37542  cdlemefs32sn1aw  37552  cdleme43fsv1snlem  37558  cdleme41sn3a  37571  cdleme32c  37581  cdleme32e  37583  cdleme32le  37585  cdleme35a  37586  cdleme35b  37588  cdleme35c  37589  cdleme35e  37591  cdleme35f  37592  cdleme36a  37598  cdleme36m  37599  cdleme39a  37603  cdleme40m  37605  cdleme40n  37606  cdleme43bN  37628  cdleme43dN  37630  cdleme46f2g2  37631  cdleme46f2g1  37632  cdleme17d2  37633  cdleme4gfv  37645  cdlemeg49le  37649  cdlemeg46c  37651  cdlemeg46fvaw  37654  cdlemeg46nlpq  37655  cdlemeg46gfre  37670  cdleme50trn2  37689  cdleme  37698  cdlemg2idN  37734  cdlemg7fvbwN  37745  cdlemg10bALTN  37774  cdlemg10a  37778  cdlemg12d  37784  cdlemg12g  37787  cdlemg12  37788  cdlemg13a  37789  cdlemg13  37790  cdlemg17b  37800  cdlemg17dN  37801  cdlemg17dALTN  37802  cdlemg17e  37803  cdlemg17f  37804  cdlemg17i  37807  cdlemg17pq  37810  cdlemg17bq  37811  cdlemg17iqN  37812  cdlemg18d  37819  cdlemg18  37820  cdlemg19a  37821  cdlemg19  37822  cdlemg21  37824  cdlemg27a  37830  cdlemg28a  37831  cdlemg31b0N  37832  cdlemg27b  37834  cdlemg31c  37837  cdlemg33b0  37839  cdlemg33c0  37840  cdlemg28  37842  cdlemg33a  37844  cdlemg33  37849  cdlemg36  37852  ltrnco  37857  cdlemg44  37871  cdlemg47  37874  tendococl  37910  tendoplcl  37919  cdlemh1  37953  cdlemh2  37954  cdlemh  37955  cdlemi  37958  tendocan  37962  cdlemk5  37974  cdlemk6  37975  cdlemk7  37986  cdlemk11  37987  cdlemk12  37988  cdlemkole  37991  cdlemk14  37992  cdlemk15  37993  cdlemk16a  37994  cdlemk16  37995  cdlemk18  38006  cdlemk19  38007  cdlemk7u  38008  cdlemk11u  38009  cdlemk12u  38010  cdlemk21N  38011  cdlemk20  38012  cdlemkoatnle-2N  38013  cdlemk13-2N  38014  cdlemkole-2N  38015  cdlemk14-2N  38016  cdlemk15-2N  38017  cdlemk16-2N  38018  cdlemk17-2N  38019  cdlemk18-2N  38024  cdlemk19-2N  38025  cdlemk7u-2N  38026  cdlemk11u-2N  38027  cdlemk12u-2N  38028  cdlemk21-2N  38029  cdlemk20-2N  38030  cdlemk22  38031  cdlemk27-3  38045  cdlemk33N  38047  cdlemk11ta  38067  cdlemkid3N  38071  cdlemk11tc  38083  cdlemk11t  38084  cdlemk45  38085  cdlemk46  38086  cdlemk47  38087  cdlemk48  38088  cdlemk49  38089  cdlemk50  38090  cdlemk51  38091  cdlemk52  38092  cdlemk53a  38093  cdlemk55b  38098  cdlemkyyN  38100  cdlemk55u1  38103  cdlemk39u1  38105  cdlemk56  38109  cdlemm10N  38256  dihord1  38356  dihord2a  38357  dihord2b  38358  dihord10  38361  dihord4  38396  dihord5apre  38400  dihglblem2N  38432  dihjatc1  38449  dihjatc2N  38450  dihjatc3  38451  dihmeetlem15N  38459  dihmeetlem20N  38464  mapdpglem24  38842  hdmap14lem11  39016  hdmap14lem12  39017  mzpsubst  39352  monotuz  39545  congmul  39571  congsub  39574  ntrclsiso  40424  ntrclskb  40426  ntrclsk3  40427  infleinf  41647  mullimc  41904  mullimcf  41911  0ellimcdiv  41937  limclner  41939  sge0xaddlem2  42723  lincdifsn  44486  itschlc0yqe  44754  itscnhlc0xyqsol  44759  itsclc0xyqsolr  44763  itsclquadeu  44771