Theorem simp1r 1199

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp11r  1286  simp21r  1292  simp31r  1298  eqfunresadj  7300  offsplitfpar  8055  poseq  8094  omeulem2  8504  uniinqs  8727  unxpdomlem3  9148  elfiun  9320  cofsmo  10166  isfin2-2  10216  isf32lem9  10258  tskun  10683  tskurn  10686  reclem3pr  10946  dedekind  11282  subaddmulsub  11586  dmdcan  11837  lt2msq1  12012  supmullem1  12098  supmul  12100  xaddass2  13155  xlt2add  13165  xmulasslem3  13191  iccsplit  13391  expaddzlem  14018  expaddz  14019  expmulz  14021  limsupgle  15390  o1add  15527  o1mul  15528  o1sub  15529  bitsfzo  16352  sadfval  16369  smufval  16394  nn0rppwr  16478  prmexpb  16636  4sqlem18  16880  vdwlem10  16908  setsstruct2  17091  mrieqv2d  17551  curf1  18137  chnccat  18538  mgmsscl  18559  mndpfsupp  18681  mndodcong  19460  subgabl  19754  gex2abl  19769  ogrpinvlt  20062  cntzsubrng  20488  cntzsubr  20527  abvres  20752  lbsind2  21021  lbsextlem2  21102  lbsextg  21105  matring  22364  mdetunilem8  22540  maducoeval  22560  maducoeval2  22561  madurid  22565  cramerimplem3  22606  pmatcollpw2  22699  pm2mpf1  22720  cnprest  23210  isreg2  23298  fbssfi  23758  hausflimlem  23900  tmdgsum  24016  ssblps  24343  ssbl  24344  xrsmopn  24734  cphassi  25147  cphassir  25148  4cphipval2  25175  cphipval  25176  dvres2  25846  vieta1  26253  aalioulem4  26276  efgh  26483  cxpadd  26621  cxpsub  26624  divcxp  26629  cxple2  26639  cxplt2  26640  cxpcn3lem  26690  angcan  26745  ang180lem5  26756  isosctrlem3  26763  lgssq  27281  nosupinfsep  27677  noetalem1  27686  noeta2  27730  sltlpss  27859  brbtwn2  28890  axcontlem4  28952  axcontlem8  28956  uhgr2edg  29193  chscllem4  31627  cshwrnid  32949  pstmval  33915  measinblem  34240  cvmlift2lem6  35359  linethru  36204  cnres2  37809  lcv1  39146  lfl1  39175  lshpkrex  39223  hlrelat3  39517  cvrval3  39518  cvrval4N  39519  athgt  39561  atcvrlln2  39624  atcvrlln  39625  lvolnle3at  39687  lvolnlelpln  39690  4atlem11  39714  4atlem12  39717  2lplnj  39725  dalemddea  39789  cdlema2N  39897  paddasslem2  39926  atmod1i1m  39963  lhp2lt  40106  lhp0lt  40108  lhpexle3lem  40116  lhpj1  40127  lhpmcvr4N  40131  lhpelim  40142  lhpmod2i2  40143  lhpmod6i1  40144  cdlemb2  40146  lhpat  40148  ltrnatb  40242  ltrnel  40244  ltrncnvel  40247  ltrncnv  40251  trlval2  40268  trljat1  40271  trljat2  40272  trlnidatb  40282  cdlemc1  40296  cdlemc2  40297  cdlemc5  40300  cdlemc6  40301  cdleme0aa  40315  cdleme0b  40317  cdleme0c  40318  cdleme0e  40322  cdleme0fN  40323  cdleme01N  40326  cdleme0ex1N  40328  cdleme0moN  40330  cdleme3g  40339  cdleme3h  40340  cdleme3  40342  cdleme4  40343  cdleme4a  40344  cdleme5  40345  cdleme8  40355  cdleme9  40358  cdleme10  40359  cdleme16aN  40364  cdleme11fN  40369  cdleme11g  40370  cdleme11k  40373  cdleme13  40377  cdleme17c  40393  cdleme17d1  40394  cdleme18c  40398  cdleme22gb  40399  cdlemeda  40403  cdlemednpq  40404  cdlemednuN  40405  cdleme19c  40410  cdleme20aN  40414  cdleme20bN  40415  cdleme20c  40416  cdleme22aa  40444  cdleme22d  40448  cdleme22e  40449  cdleme27cl  40471  cdleme27a  40472  cdleme30a  40483  cdleme42a  40576  cdleme42c  40577  cdlemg2fv2  40705  cdlemg2m  40709  cdlemg4g  40721  cdlemg4  40722  cdlemg6c  40725  cdlemg7aN  40730  cdlemg9a  40737  cdlemg9b  40738  cdlemg10c  40744  cdlemg12a  40748  cdlemg12b  40749  cdlemg17a  40766  cdlemg18b  40784  cdlemg18c  40785  trlcoabs2N  40827  trlcolem  40831  tendoco2  40873  tendoicl  40901  cdlemi1  40923  cdlemi2  40924  cdlemj3  40928  tendocan  40929  cdlemk3  40938  cdlemk4  40939  cdlemk5a  40940  cdlemk9  40944  cdlemk9bN  40945  cdlemk10  40948  cdlemk30  40999  cdlemk31  41001  cdlemk39  41021  cdlemkfid1N  41026  cdlemkfid2N  41028  cdlemk19ylem  41035  cdlemk19xlem  41047  cdlemk53b  41061  cdlemk53  41062  cdlemk55a  41064  cdlemk43N  41068  cdlemk19u1  41074  cdlemm10N  41223  cdlemn2  41300  cdlemn10  41311  dihjustlem  41321  dihord2cN  41326  dihvalcq2  41352  dihopelvalcpre  41353  dihord5b  41364  dihord6b  41365  dihmeetlem2N  41404  dihmeetbclemN  41409  dihmeetlem4preN  41411  dihmeetALTN  41432  dochshpncl  41489  dochsatshpb  41557  hdmapval3N  41943  hgmap11  42007  f1o2d2  42332  remulcand  42538  pellfundex  42984  congtr  43063  fzmaxdif  43079  isnumbasgrplem2  43202  idomsubgmo  43291  ntrclsk13  44169  grumnudlem  44383  restuni3  45220  unirnmapsn  45316  ssmapsn  45318  infnsuprnmpt  45352  upbdrech  45411  suplesup  45443  infleinf  45475  supxrunb3  45502  mullimc  45721  islptre  45724  mullimcf  45728  neglimc  45750  limsupmnfuzlem  45829  limsupre3lem  45835  limsupre3uzlem  45838  icccncfext  45990  dvmptfprod  46048  stoweidlem31  46134  opnvonmbllem2  46736  smflimsuplem7  46929  ormkglobd  46978  funressneu  47152  cfsetsnfsetf1  47164  prmdvdsfmtnof1lem1  47689  uhgrimisgrgriclem  48035  clnbgrgrim  48039  grlimedgclnbgr  48100  domnmsuppn0  48474  lincext3  48562  2arymaptfo  48760