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 734	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  8085  tfrlem1  8315  injresinj  13746  swrdccatin1  14687  reuccatpfxs1  14709  prdsval  17418  catcocl  17651  catass  17652  catpropd  17675  cidpropd  17676  monpropd  17704  subccocl  17812  funcco  17838  funcpropd  17869  fucpropd  17947  initoeu2lem1  17981  xpcpropd  18174  curf2ndf  18213  drsdirfi  18271  chnind  18587  chnub  18588  chnso  18590  mhmmnd  19040  ghmqusnsg  19257  ghmquskerlem3  19261  gsmsymgreqlem2  19406  dfod2  19539  ghmcmn  19806  omndmul2  20108  rhmqusnsg  21283  psgndif  21582  dmatscmcl  22468  smatvscl  22489  cpmatmcllem  22683  pm2mpmhmlem2  22784  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  neitr  23145  1stcrest  23418  dissnref  23493  dissnlocfin  23494  neitx  23572  tgqtop  23677  ptcmplem3  24019  trust  24194  utoptop  24199  restutopopn  24203  ustuqtop2  24207  ustuqtop4  24209  utop3cls  24216  met1stc  24486  prdsxmslem2  24494  metustexhalf  24521  cfilucfil  24524  metucn  24536  aannenlem1  26294  ulmuni  26357  lgamucov  27001  2sqmo  27400  pntpbnd  27551  pntlem3  27572  noetasuplem4  27700  noetainflem4  27704  bdayfinbndlem1  28459  tgbtwndiff  28574  tgifscgr  28576  iscgrglt  28582  tgbtwnconn1lem3  28642  tgbtwnconn1  28643  legov  28653  legtrd  28657  legtri3  28658  ltgseg  28664  legso  28667  tglinethru  28704  tglnpt2  28709  colline  28717  miriso  28738  midexlem  28760  perpneq  28782  isperp2  28783  footexALT  28786  footex  28789  midex  28805  opphllem3  28817  opphl  28822  hlpasch  28824  lnopp2hpgb  28831  lmieu  28852  trgcopyeu  28874  dfcgra2  28898  f1otrg  28939  axcontlem2  29034  2pthon3v  30011  2ndresdju  32722  fnpreimac  32743  fsumiunle  32902  ressprs  33026  dfmgc2  33056  mgcf1o  33063  mndlrinvb  33085  mndlactf1o  33090  gsumfs2d  33122  gsumwun  33137  gsumwrd2dccatlem  33138  tocyccntz  33205  cyc3genpm  33213  cycpmconjs  33217  cyc3conja  33218  isarchi3  33248  isarchiofld  33260  elrgspnlem4  33306  erler  33326  elrlocbasi  33327  rlocaddval  33329  rlocmulval  33330  rloccring  33331  rlocf1  33334  isdrng4  33356  fracfld  33369  imaslmod  33413  dvdsruasso  33445  nsgqusf1olem1  33473  nsgqusf1olem3  33475  lmhmqusker  33477  intlidl  33480  rhmquskerlem  33485  elrspunidl  33488  elrspunsn  33489  idlinsubrg  33491  rhmimaidl  33492  drngidl  33493  isprmidlc  33507  rhmpreimaprmidl  33511  qsidomlem2  33513  ssdifidllem  33516  ssdifidlprm  33518  mxidlprm  33530  mxidlirredi  33531  ssmxidllem  33533  ssmxidl  33534  opprqusplusg  33549  opprqusmulr  33551  qsdrngi  33555  qsdrng  33557  rsprprmprmidlb  33583  rprmdvdsprod  33594  1arithidom  33597  1arithufdlem2  33605  1arithufdlem3  33606  dfufd2lem  33609  r1plmhm  33670  r1pquslmic  33671  lbsdiflsp0  33770  dimkerim  33771  fedgmul  33775  fldextrspunlsplem  33817  extdgfialg  33838  constrconj  33889  constrfin  33890  constrelextdg2  33891  constrextdg2lem  33892  constrfiss  33895  ist0cld  33977  txomap  33978  qtophaus  33980  zarcls1  34013  zarclsint  34016  zarclssn  34017  pstmxmet  34041  sqsscirc1  34052  lmxrge0  34096  esumcst  34207  esumfsup  34214  esum2dlem  34236  esum2d  34237  esumiun  34238  ldsysgenld  34304  sigapildsys  34306  omssubadd  34444  signstfvneq0  34716  actfunsnf1o  34748  afsval  34815  nn0prpwlem  36504  lindsenlbs  37936  matunitlindflem1  37937  matunitlindflem2  37938  mblfinlem3  37980  itg2addnclem  37992  sstotbnd2  38095  prdstotbnd  38115  lcfl8  41948  fldhmf1  42529  mndmolinv  42534  primrootscoprmpow  42538  primrootspoweq0  42545  aks6d1c2p2  42558  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c5  42578  aks6d1c6lem3  42611  unitscyglem3  42636  fiabv  42981  dffltz  43067  flt4lem7  43092  nna4b4nsq  43093  diophren  43241  rencldnfilem  43248  pellex  43263  pell1234qrdich  43289  pell1qrgap  43302  pellfundex  43314  omabs2  43760  iunconnlem2  45361  modelaxrep  45408  suplesup  45769  infleinflem2  45800  xrralrecnnle  45812  rexabslelem  45846  limcrecl  46059  limcleqr  46072  0ellimcdiv  46077  limclner  46079  limsupubuz  46141  limsupvaluz2  46166  supcnvlimsup  46168  climxrre  46178  xlimmnfvlem2  46261  xlimmnfv  46262  xlimpnfvlem2  46265  xlimpnfv  46266  icccncfext  46315  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  fourierdlem50  46584  fourierdlem51  46585  fourierdlem80  46614  fourierdlem87  46621  fourierdlem103  46637  fourierdlem104  46638  meaiuninc3v  46912  omef  46924  smflimlem2  47200  smflimlem4  47202  smfmullem3  47221  fsupdm  47270  finfdm  47274  chnerlem1  47312  imaf1co  49630  upfval  49651  fuco21  49811  prcofvalg  49851