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  8071  tfrlem1  8301  injresinj  13693  swrdccatin1  14634  reuccatpfxs1  14656  prdsval  17361  catcocl  17593  catass  17594  catpropd  17617  cidpropd  17618  monpropd  17646  subccocl  17754  funcco  17780  funcpropd  17811  fucpropd  17889  initoeu2lem1  17923  xpcpropd  18116  curf2ndf  18155  drsdirfi  18213  chnind  18529  chnub  18530  chnso  18532  mhmmnd  18979  ghmqusnsg  19196  ghmquskerlem3  19200  gsmsymgreqlem2  19345  dfod2  19478  ghmcmn  19745  omndmul2  20047  rhmqusnsg  21224  psgndif  21541  dmatscmcl  22419  smatvscl  22440  cpmatmcllem  22634  pm2mpmhmlem2  22735  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  neitr  23096  1stcrest  23369  dissnref  23444  dissnlocfin  23445  neitx  23523  tgqtop  23628  ptcmplem3  23970  trust  24145  utoptop  24150  restutopopn  24154  ustuqtop2  24158  ustuqtop4  24160  utop3cls  24167  met1stc  24437  prdsxmslem2  24445  metustexhalf  24472  cfilucfil  24475  metucn  24487  aannenlem1  26264  ulmuni  26329  lgamucov  26976  2sqmo  27376  pntpbnd  27527  pntlem3  27548  noetasuplem4  27676  noetainflem4  27680  tgbtwndiff  28485  tgifscgr  28487  iscgrglt  28493  tgbtwnconn1lem3  28553  tgbtwnconn1  28554  legov  28564  legtrd  28568  legtri3  28569  ltgseg  28575  legso  28578  tglinethru  28615  tglnpt2  28620  colline  28628  miriso  28649  midexlem  28671  perpneq  28693  isperp2  28694  footexALT  28697  footex  28700  midex  28716  opphllem3  28728  opphl  28733  hlpasch  28735  lnopp2hpgb  28742  lmieu  28763  trgcopyeu  28785  dfcgra2  28809  f1otrg  28850  axcontlem2  28945  2pthon3v  29923  2ndresdju  32633  fnpreimac  32655  fsumiunle  32817  ressprs  32954  dfmgc2  32984  mgcf1o  32991  mndlrinvb  33013  mndlactf1o  33018  gsumfs2d  33042  gsumwun  33052  gsumwrd2dccatlem  33053  tocyccntz  33120  cyc3genpm  33128  cycpmconjs  33132  cyc3conja  33133  isarchi3  33163  isarchiofld  33175  elrgspnlem4  33219  erler  33239  elrlocbasi  33240  rlocaddval  33242  rlocmulval  33243  rloccring  33244  rlocf1  33247  isdrng4  33268  fracfld  33281  imaslmod  33325  dvdsruasso  33357  nsgqusf1olem1  33385  nsgqusf1olem3  33387  lmhmqusker  33389  intlidl  33392  rhmquskerlem  33397  elrspunidl  33400  elrspunsn  33401  idlinsubrg  33403  rhmimaidl  33404  drngidl  33405  isprmidlc  33419  rhmpreimaprmidl  33423  qsidomlem2  33425  ssdifidllem  33428  ssdifidlprm  33430  mxidlprm  33442  mxidlirredi  33443  ssmxidllem  33445  ssmxidl  33446  opprqusplusg  33461  opprqusmulr  33463  qsdrngi  33467  qsdrng  33469  rsprprmprmidlb  33495  rprmdvdsprod  33506  1arithidom  33509  1arithufdlem2  33517  1arithufdlem3  33518  dfufd2lem  33521  r1plmhm  33577  r1pquslmic  33578  lbsdiflsp0  33660  dimkerim  33661  fedgmul  33665  fldextrspunlsplem  33707  extdgfialg  33728  constrconj  33779  constrfin  33780  constrelextdg2  33781  constrextdg2lem  33782  constrfiss  33785  ist0cld  33867  txomap  33868  qtophaus  33870  zarcls1  33903  zarclsint  33906  zarclssn  33907  pstmxmet  33931  sqsscirc1  33942  lmxrge0  33986  esumcst  34097  esumfsup  34104  esum2dlem  34126  esum2d  34127  esumiun  34128  ldsysgenld  34194  sigapildsys  34196  omssubadd  34334  signstfvneq0  34606  actfunsnf1o  34638  afsval  34705  nn0prpwlem  36387  lindsenlbs  37675  matunitlindflem1  37676  matunitlindflem2  37677  mblfinlem3  37719  itg2addnclem  37731  sstotbnd2  37834  prdstotbnd  37854  lcfl8  41621  fldhmf1  42203  mndmolinv  42208  primrootscoprmpow  42212  primrootspoweq0  42219  aks6d1c2p2  42232  aks6d1c2lem4  42240  aks6d1c2  42243  aks6d1c5  42252  aks6d1c6lem3  42285  unitscyglem3  42310  fiabv  42654  dffltz  42752  flt4lem7  42777  nna4b4nsq  42778  diophren  42930  rencldnfilem  42937  pellex  42952  pell1234qrdich  42978  pell1qrgap  42991  pellfundex  43003  omabs2  43449  iunconnlem2  45051  modelaxrep  45098  suplesup  45462  infleinflem2  45493  xrralrecnnle  45505  rexabslelem  45540  limcrecl  45753  limcleqr  45766  0ellimcdiv  45771  limclner  45773  limsupubuz  45835  limsupvaluz2  45860  supcnvlimsup  45862  climxrre  45872  xlimmnfvlem2  45955  xlimmnfv  45956  xlimpnfvlem2  45959  xlimpnfv  45960  icccncfext  46009  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  fourierdlem50  46278  fourierdlem51  46279  fourierdlem80  46308  fourierdlem87  46315  fourierdlem103  46331  fourierdlem104  46332  meaiuninc3v  46606  omef  46618  smflimlem2  46894  smflimlem4  46896  smfmullem3  46915  fsupdm  46964  finfdm  46968  chnerlem1  47004  imaf1co  49280  upfval  49301  fuco21  49461  prcofvalg  49501