Theorem simp-4r 783

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-4r	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp-4r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad4antlr 733	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  fimaproj  8077  tfrlem1  8307  injresinj  13707  swrdccatin1  14648  reuccatpfxs1  14670  prdsval  17375  catcocl  17608  catass  17609  catpropd  17632  cidpropd  17633  monpropd  17661  subccocl  17769  funcco  17795  funcpropd  17826  fucpropd  17904  initoeu2lem1  17938  xpcpropd  18131  curf2ndf  18170  drsdirfi  18228  chnind  18544  chnub  18545  chnso  18547  mhmmnd  18994  ghmqusnsg  19211  ghmquskerlem3  19215  gsmsymgreqlem2  19360  dfod2  19493  ghmcmn  19760  omndmul2  20062  rhmqusnsg  21240  psgndif  21557  dmatscmcl  22447  smatvscl  22468  cpmatmcllem  22662  pm2mpmhmlem2  22763  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  neitr  23124  1stcrest  23397  dissnref  23472  dissnlocfin  23473  neitx  23551  tgqtop  23656  ptcmplem3  23998  trust  24173  utoptop  24178  restutopopn  24182  ustuqtop2  24186  ustuqtop4  24188  utop3cls  24195  met1stc  24465  prdsxmslem2  24473  metustexhalf  24500  cfilucfil  24503  metucn  24515  aannenlem1  26292  ulmuni  26357  lgamucov  27004  2sqmo  27404  pntpbnd  27555  pntlem3  27576  noetasuplem4  27704  noetainflem4  27708  bdayfinbndlem1  28463  tgbtwndiff  28578  tgifscgr  28580  iscgrglt  28586  tgbtwnconn1lem3  28646  tgbtwnconn1  28647  legov  28657  legtrd  28661  legtri3  28662  ltgseg  28668  legso  28671  tglinethru  28708  tglnpt2  28713  colline  28721  miriso  28742  midexlem  28764  perpneq  28786  isperp2  28787  footexALT  28790  footex  28793  midex  28809  opphllem3  28821  opphl  28826  hlpasch  28828  lnopp2hpgb  28835  lmieu  28856  trgcopyeu  28878  dfcgra2  28902  f1otrg  28943  axcontlem2  29038  2pthon3v  30016  2ndresdju  32727  fnpreimac  32749  fsumiunle  32910  ressprs  33048  dfmgc2  33078  mgcf1o  33085  mndlrinvb  33107  mndlactf1o  33112  gsumfs2d  33144  gsumwun  33158  gsumwrd2dccatlem  33159  tocyccntz  33226  cyc3genpm  33234  cycpmconjs  33238  cyc3conja  33239  isarchi3  33269  isarchiofld  33281  elrgspnlem4  33327  erler  33347  elrlocbasi  33348  rlocaddval  33350  rlocmulval  33351  rloccring  33352  rlocf1  33355  isdrng4  33377  fracfld  33390  imaslmod  33434  dvdsruasso  33466  nsgqusf1olem1  33494  nsgqusf1olem3  33496  lmhmqusker  33498  intlidl  33501  rhmquskerlem  33506  elrspunidl  33509  elrspunsn  33510  idlinsubrg  33512  rhmimaidl  33513  drngidl  33514  isprmidlc  33528  rhmpreimaprmidl  33532  qsidomlem2  33534  ssdifidllem  33537  ssdifidlprm  33539  mxidlprm  33551  mxidlirredi  33552  ssmxidllem  33554  ssmxidl  33555  opprqusplusg  33570  opprqusmulr  33572  qsdrngi  33576  qsdrng  33578  rsprprmprmidlb  33604  rprmdvdsprod  33615  1arithidom  33618  1arithufdlem2  33626  1arithufdlem3  33627  dfufd2lem  33630  r1plmhm  33691  r1pquslmic  33692  lbsdiflsp0  33783  dimkerim  33784  fedgmul  33788  fldextrspunlsplem  33830  extdgfialg  33851  constrconj  33902  constrfin  33903  constrelextdg2  33904  constrextdg2lem  33905  constrfiss  33908  ist0cld  33990  txomap  33991  qtophaus  33993  zarcls1  34026  zarclsint  34029  zarclssn  34030  pstmxmet  34054  sqsscirc1  34065  lmxrge0  34109  esumcst  34220  esumfsup  34227  esum2dlem  34249  esum2d  34250  esumiun  34251  ldsysgenld  34317  sigapildsys  34319  omssubadd  34457  signstfvneq0  34729  actfunsnf1o  34761  afsval  34828  nn0prpwlem  36516  lindsenlbs  37812  matunitlindflem1  37813  matunitlindflem2  37814  mblfinlem3  37856  itg2addnclem  37868  sstotbnd2  37971  prdstotbnd  37991  lcfl8  41758  fldhmf1  42340  mndmolinv  42345  primrootscoprmpow  42349  primrootspoweq0  42356  aks6d1c2p2  42369  aks6d1c2lem4  42377  aks6d1c2  42380  aks6d1c5  42389  aks6d1c6lem3  42422  unitscyglem3  42447  fiabv  42787  dffltz  42873  flt4lem7  42898  nna4b4nsq  42899  diophren  43051  rencldnfilem  43058  pellex  43073  pell1234qrdich  43099  pell1qrgap  43112  pellfundex  43124  omabs2  43570  iunconnlem2  45171  modelaxrep  45218  suplesup  45580  infleinflem2  45611  xrralrecnnle  45623  rexabslelem  45658  limcrecl  45871  limcleqr  45884  0ellimcdiv  45889  limclner  45891  limsupubuz  45953  limsupvaluz2  45978  supcnvlimsup  45980  climxrre  45990  xlimmnfvlem2  46073  xlimmnfv  46074  xlimpnfvlem2  46077  xlimpnfv  46078  icccncfext  46127  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  fourierdlem50  46396  fourierdlem51  46397  fourierdlem80  46426  fourierdlem87  46433  fourierdlem103  46449  fourierdlem104  46450  meaiuninc3v  46724  omef  46736  smflimlem2  47012  smflimlem4  47014  smfmullem3  47033  fsupdm  47082  finfdm  47086  chnerlem1  47122  imaf1co  49396  upfval  49417  fuco21  49577  prcofvalg  49617