Theorem simp1r 1194

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1r	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Proof of Theorem simp1r

Step	Hyp	Ref	Expression
1		simpr 487	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
2	1	3ad2ant1 1129	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398   ∧ 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:  simp11r  1281  simp21r  1287  simp31r  1293  offsplitfpar  7815  omeulem2  8209  uniinqs  8377  unxpdomlem3  8724  elfiun  8894  cofsmo  9691  isfin2-2  9741  isf32lem9  9783  tskun  10208  tskurn  10211  reclem3pr  10471  dedekind  10803  subaddmulsub  11103  dmdcan  11350  lt2msq1  11524  supmullem1  11611  supmul  11613  xaddass2  12644  xlt2add  12654  xmulasslem3  12680  iccsplit  12872  expaddzlem  13473  expaddz  13474  expmulz  13476  limsupgle  14834  o1add  14970  o1mul  14971  o1sub  14972  bitsfzo  15784  sadfval  15801  smufval  15826  prmexpb  16062  4sqlem18  16298  vdwlem10  16326  setsstruct2  16521  mrieqv2d  16910  curf1  17475  mgmsscl  17857  mndodcong  18670  subgabl  18956  gex2abl  18971  cntzsubr  19568  abvres  19610  lbsind2  19853  lbsextlem2  19931  lbsextg  19934  matring  21052  mdetunilem8  21228  maducoeval  21248  maducoeval2  21249  madurid  21253  cramerimplem3  21294  pmatcollpw2  21386  pm2mpf1  21407  cnprest  21897  isreg2  21985  fbssfi  22445  hausflimlem  22587  tmdgsum  22703  ssblps  23032  ssbl  23033  xrsmopn  23420  cphassi  23818  cphassir  23819  4cphipval2  23845  cphipval  23846  dvres2  24510  vieta1  24901  aalioulem4  24924  efgh  25125  cxpadd  25262  cxpsub  25265  divcxp  25270  cxple2  25280  cxplt2  25281  cxpcn3lem  25328  angcan  25380  ang180lem5  25391  isosctrlem3  25398  lgssq  25913  brbtwn2  26691  axcontlem4  26753  axcontlem8  26757  uhgr2edg  26990  chscllem4  29417  cshwrnid  30635  ogrpinvlt  30724  pstmval  31135  measinblem  31479  cvmlift2lem6  32555  eqfunresadj  33004  poseq  33095  noetalem5  33221  linethru  33614  cnres2  35056  lcv1  36192  lfl1  36221  lshpkrex  36269  hlrelat3  36563  cvrval3  36564  cvrval4N  36565  athgt  36607  atcvrlln2  36670  atcvrlln  36671  lvolnle3at  36733  lvolnlelpln  36736  4atlem11  36760  4atlem12  36763  2lplnj  36771  dalemddea  36835  cdlema2N  36943  paddasslem2  36972  atmod1i1m  37009  lhp2lt  37152  lhp0lt  37154  lhpexle3lem  37162  lhpj1  37173  lhpmcvr4N  37177  lhpelim  37188  lhpmod2i2  37189  lhpmod6i1  37190  cdlemb2  37192  lhpat  37194  ltrnatb  37288  ltrnel  37290  ltrncnvel  37293  ltrncnv  37297  trlval2  37314  trljat1  37317  trljat2  37318  trlnidatb  37328  cdlemc1  37342  cdlemc2  37343  cdlemc5  37346  cdlemc6  37347  cdleme0aa  37361  cdleme0b  37363  cdleme0c  37364  cdleme0e  37368  cdleme0fN  37369  cdleme01N  37372  cdleme0ex1N  37374  cdleme0moN  37376  cdleme3g  37385  cdleme3h  37386  cdleme3  37388  cdleme4  37389  cdleme4a  37390  cdleme5  37391  cdleme8  37401  cdleme9  37404  cdleme10  37405  cdleme16aN  37410  cdleme11fN  37415  cdleme11g  37416  cdleme11k  37419  cdleme13  37423  cdleme17c  37439  cdleme17d1  37440  cdleme18c  37444  cdleme22gb  37445  cdlemeda  37449  cdlemednpq  37450  cdlemednuN  37451  cdleme19c  37456  cdleme20aN  37460  cdleme20bN  37461  cdleme20c  37462  cdleme22aa  37490  cdleme22d  37494  cdleme22e  37495  cdleme27cl  37517  cdleme27a  37518  cdleme30a  37529  cdleme42a  37622  cdleme42c  37623  cdlemg2fv2  37751  cdlemg2m  37755  cdlemg4g  37767  cdlemg4  37768  cdlemg6c  37771  cdlemg7aN  37776  cdlemg9a  37783  cdlemg9b  37784  cdlemg10c  37790  cdlemg12a  37794  cdlemg12b  37795  cdlemg17a  37812  cdlemg18b  37830  cdlemg18c  37831  trlcoabs2N  37873  trlcolem  37877  tendoco2  37919  tendoicl  37947  cdlemi1  37969  cdlemi2  37970  cdlemj3  37974  tendocan  37975  cdlemk3  37984  cdlemk4  37985  cdlemk5a  37986  cdlemk9  37990  cdlemk9bN  37991  cdlemk10  37994  cdlemk30  38045  cdlemk31  38047  cdlemk39  38067  cdlemkfid1N  38072  cdlemkfid2N  38074  cdlemk19ylem  38081  cdlemk19xlem  38093  cdlemk53b  38107  cdlemk53  38108  cdlemk55a  38110  cdlemk43N  38114  cdlemk19u1  38120  cdlemm10N  38269  cdlemn2  38346  cdlemn10  38357  dihjustlem  38367  dihord2cN  38372  dihvalcq2  38398  dihopelvalcpre  38399  dihord5b  38410  dihord6b  38411  dihmeetlem2N  38450  dihmeetbclemN  38455  dihmeetlem4preN  38457  dihmeetALTN  38478  dochshpncl  38535  dochsatshpb  38603  hdmapval3N  38989  hgmap11  39053  nn0rppwr  39202  remulcand  39270  pellfundex  39503  congtr  39582  fzmaxdif  39598  isnumbasgrplem2  39724  idomsubgmo  39818  ntrclsk13  40441  grumnudlem  40641  restuni3  41404  unirnmapsn  41497  ssmapsn  41499  infnsuprnmpt  41542  upbdrech  41592  suplesup  41627  infleinf  41660  supxrunb3  41692  mullimc  41917  islptre  41920  mullimcf  41924  neglimc  41948  limsupmnfuzlem  42027  limsupre3lem  42033  limsupre3uzlem  42036  icccncfext  42190  dvmptfprod  42250  stoweidlem31  42336  opnvonmbllem2  42935  smflimsuplem7  43120  funressneu  43302  prmdvdsfmtnof1lem1  43766  domnmsuppn0  44437  mndpfsupp  44444  lincext3  44531