Theorem simp-4r 784

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  8160  tfrlem1  8416  injresinj  13827  swrdccatin1  14763  reuccatpfxs1  14785  prdsval  17500  catcocl  17728  catass  17729  catpropd  17752  cidpropd  17753  monpropd  17781  subccocl  17890  funcco  17916  funcpropd  17947  fucpropd  18025  initoeu2lem1  18059  xpcpropd  18253  curf2ndf  18292  drsdirfi  18351  mhmmnd  19082  ghmqusnsg  19300  ghmquskerlem3  19304  gsmsymgreqlem2  19449  dfod2  19582  ghmcmn  19849  rhmqusnsg  21295  psgndif  21620  dmatscmcl  22509  smatvscl  22530  cpmatmcllem  22724  pm2mpmhmlem2  22825  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  neitr  23188  1stcrest  23461  dissnref  23536  dissnlocfin  23537  neitx  23615  tgqtop  23720  ptcmplem3  24062  trust  24238  utoptop  24243  restutopopn  24247  ustuqtop2  24251  ustuqtop4  24253  utop3cls  24260  met1stc  24534  prdsxmslem2  24542  metustexhalf  24569  cfilucfil  24572  metucn  24584  aannenlem1  26370  ulmuni  26435  lgamucov  27081  2sqmo  27481  pntpbnd  27632  pntlem3  27653  noetasuplem4  27781  noetainflem4  27785  tgbtwndiff  28514  tgifscgr  28516  iscgrglt  28522  tgbtwnconn1lem3  28582  tgbtwnconn1  28583  legov  28593  legtrd  28597  legtri3  28598  ltgseg  28604  legso  28607  tglinethru  28644  tglnpt2  28649  colline  28657  miriso  28678  midexlem  28700  perpneq  28722  isperp2  28723  footexALT  28726  footex  28729  midex  28745  opphllem3  28757  opphl  28762  hlpasch  28764  lnopp2hpgb  28771  lmieu  28792  trgcopyeu  28814  dfcgra2  28838  f1otrg  28879  axcontlem2  28980  2pthon3v  29963  2ndresdju  32659  fnpreimac  32681  fsumiunle  32831  ressprs  32954  dfmgc2  32986  mgcf1o  32993  chnind  33001  chnub  33002  chnso  33004  mndlrinvb  33030  mndlactf1o  33035  gsumfs2d  33058  gsumwun  33068  gsumwrd2dccatlem  33069  omndmul2  33089  tocyccntz  33164  cyc3genpm  33172  cycpmconjs  33176  cyc3conja  33177  isarchi3  33194  elrgspnlem4  33249  erler  33269  elrlocbasi  33270  rlocaddval  33272  rlocmulval  33273  rloccring  33274  rlocf1  33277  isdrng4  33298  fracfld  33310  isarchiofld  33347  imaslmod  33381  dvdsruasso  33413  nsgqusf1olem1  33441  nsgqusf1olem3  33443  lmhmqusker  33445  intlidl  33448  rhmquskerlem  33453  elrspunidl  33456  elrspunsn  33457  idlinsubrg  33459  rhmimaidl  33460  drngidl  33461  isprmidlc  33475  rhmpreimaprmidl  33479  qsidomlem2  33481  ssdifidllem  33484  ssdifidlprm  33486  mxidlprm  33498  mxidlirredi  33499  ssmxidllem  33501  ssmxidl  33502  opprqusplusg  33517  opprqusmulr  33519  qsdrngi  33523  qsdrng  33525  rsprprmprmidlb  33551  rprmdvdsprod  33562  1arithidom  33565  1arithufdlem2  33573  1arithufdlem3  33574  dfufd2lem  33577  r1plmhm  33630  r1pquslmic  33631  lbsdiflsp0  33677  dimkerim  33678  fedgmul  33682  fldextrspunlsplem  33723  constrconj  33786  constrfin  33787  constrelextdg2  33788  constrextdg2lem  33789  ist0cld  33832  txomap  33833  qtophaus  33835  zarcls1  33868  zarclsint  33871  zarclssn  33872  pstmxmet  33896  sqsscirc1  33907  lmxrge0  33951  esumcst  34064  esumfsup  34071  esum2dlem  34093  esum2d  34094  esumiun  34095  ldsysgenld  34161  sigapildsys  34163  omssubadd  34302  signstfvneq0  34587  actfunsnf1o  34619  afsval  34686  nn0prpwlem  36323  lindsenlbs  37622  matunitlindflem1  37623  matunitlindflem2  37624  mblfinlem3  37666  itg2addnclem  37678  sstotbnd2  37781  prdstotbnd  37801  lcfl8  41504  fldhmf1  42091  mndmolinv  42096  primrootscoprmpow  42100  primrootspoweq0  42107  aks6d1c2p2  42120  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c5  42140  aks6d1c6lem3  42173  unitscyglem3  42198  fiabv  42546  dffltz  42644  flt4lem7  42669  nna4b4nsq  42670  diophren  42824  rencldnfilem  42831  pellex  42846  pell1234qrdich  42872  pell1qrgap  42885  pellfundex  42897  omabs2  43345  iunconnlem2  44955  modelaxrep  44998  suplesup  45350  infleinflem2  45382  xrralrecnnle  45394  rexabslelem  45429  limcrecl  45644  limcleqr  45659  0ellimcdiv  45664  limclner  45666  limsupubuz  45728  limsupvaluz2  45753  supcnvlimsup  45755  climxrre  45765  xlimmnfvlem2  45848  xlimmnfv  45849  xlimpnfvlem2  45852  xlimpnfv  45853  icccncfext  45902  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  fourierdlem50  46171  fourierdlem51  46172  fourierdlem80  46201  fourierdlem87  46208  fourierdlem103  46224  fourierdlem104  46225  meaiuninc3v  46499  omef  46511  smflimlem2  46787  smflimlem4  46789  smfmullem3  46808  fsupdm  46857  finfdm  46861  upfval  48933  fuco21  49031