Theorem simp-4r 795

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 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad4antlr 745	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fimaproj  8131  tfrlem1  8362  injresinj  13820  swrdccatin1  14762  reuccatpfxs1  14784  prdsval  17508  catcocl  17741  catass  17742  catpropd  17765  cidpropd  17766  monpropd  17794  subccocl  17902  funcco  17928  funcpropd  17959  fucpropd  18037  initoeu2lem1  18071  xpcpropd  18264  curf2ndf  18303  drsdirfi  18361  chnind  18677  chnub  18678  chnso  18680  mhmmnd  19130  ghmqusnsg  19352  ghmquskerlem3  19356  gsmsymgreqlem2  19501  dfod2  19634  ghmcmn  19901  omndmul2  20203  rhmqusnsg  21396  isprmidlc  21443  rhmpreimaprmidl  21448  qsidomlem2  21450  ssdifidllem  21453  ssdifidlprm  21455  psgndif  21721  dmatscmcl  22629  smatvscl  22650  cpmatmcllem  22844  pm2mpmhmlem2  22945  chfacfscmulgsum  22986  chfacfpmmulgsum  22990  neitr  23306  1stcrest  23579  dissnref  23654  dissnlocfin  23655  neitx  23733  tgqtop  23838  ptcmplem3  24180  trust  24355  utoptop  24360  restutopopn  24364  ustuqtop2  24368  ustuqtop4  24370  utop3cls  24377  met1stc  24647  prdsxmslem2  24655  metustexhalf  24682  cfilucfil  24685  metucn  24697  aannenlem1  26458  ulmuni  26521  lgamucov  27168  2sqmo  27567  pntpbnd  27718  pntlem3  27739  noetasuplem4  27866  noetainflem4  27870  bdayfinbndlem1  28626  tgbtwndiff  28741  tgifscgr  28743  iscgrglt  28749  tgbtwnconn1lem3  28809  tgbtwnconn1  28810  legov  28820  legtrd  28824  legtri3  28825  ltgseg  28831  legso  28834  tglinethru  28871  tglinesseq  28875  colline  28885  tglnpt2  28888  tglnpt4  28890  miriso  28909  midexlem  28931  perpneq  28953  isperp2  28954  footexALT  28957  footex  28960  midex  28977  opphllem3  28989  opphl  28994  hlpasch  28997  lnopp2hpgb  29004  plngcplem  29025  lnssplng  29032  plng3p  29037  lmieu  29051  trgcopyeu  29074  dfcgra2  29098  ragcgra  29103  prlnghpg  29151  perpprlng  29153  prlngex  29154  prlngmolem1  29155  prlngmolem2  29156  f1otrg  29161  axcontlem2  29256  2pthon3v  30233  2ndresdju  32935  fnpreimac  32956  fsumiunle  33114  ressprs  33227  dfmgc2  33257  mgcf1o  33264  mndlrinvb  33286  mndlactf1o  33291  gsumfs2d  33322  gsumwun  33337  gsumwrd2dccatlem  33338  tocyccntz  33405  cyc3genpm  33413  cycpmconjs  33417  cyc3conja  33418  isarchi3  33448  isarchiofld  33460  elrgspnlem4  33506  erler  33526  elrlocbasi  33528  rlocaddval  33530  rlocmulval  33531  rloccring  33532  rlocf1  33535  rlocisunit  33537  ricdomn1  33550  isdrng4  33559  fracfld  33572  imaslmod  33616  dvdsruasso  33642  nsgqusf1olem1  33666  nsgqusf1olem3  33668  lmhmqusker  33670  intlidl  33672  rhmquskerlem  33677  elrspunidl  33680  elrspunsn  33681  idlinsubrg  33683  rhmimaidl  33684  drngidl  33685  mxidlprm  33698  mxidlirredi  33699  ssmxidllem  33701  ssmxidl  33702  opprqusplusg  33716  opprqusmulr  33718  qsdrngi  33722  qsdrng  33724  drnglring  33727  dflring2  33728  dflringlem3  33731  dflring4  33733  rsprprmprmidlb  33758  rprmdvdsprod  33769  1arithidom  33772  1arithufdlem2  33780  1arithufdlem3  33781  dfufd2lem  33784  r1plmhm  33844  r1pquslmic  33845  mplidomlem  33862  lbsdiflsp0  33961  dimkerim  33962  fedgmul  33966  fldextrspunlsplem  34008  extdgfialg  34029  constrconj  34080  constrfin  34081  constrelextdg2  34082  constrextdg2lem  34083  constrfiss  34086  ist0cld  34168  txomap  34169  qtophaus  34171  zarcls1  34204  zarclsint  34207  zarclssn  34208  pstmxmet  34232  sqsscirc1  34243  lmxrge0  34287  esumcst  34398  esumfsup  34405  esum2dlem  34427  esum2d  34428  esumiun  34429  ldsysgenld  34495  sigapildsys  34497  omssubadd  34635  signstfvneq0  34904  actfunsnf1o  34936  afsval  35006  nn0prpwlem  36722  lindsenlbs  38154  matunitlindflem1  38155  matunitlindflem2  38156  mblfinlem3  38198  itg2addnclem  38210  sstotbnd2  38313  prdstotbnd  38333  lcfl8  42166  fldhmf1  42747  mndmolinv  42752  primrootscoprmpow  42756  primrootspoweq0  42763  aks6d1c2p2  42776  aks6d1c2lem4  42784  aks6d1c2  42787  aks6d1c5  42796  aks6d1c6lem3  42829  unitscyglem3  42854  fiabv  43196  dffltz  43258  flt4lem7  43283  nna4b4nsq  43284  diophren  43432  rencldnfilem  43439  pellex  43454  pell1234qrdich  43480  pell1qrgap  43493  pellfundex  43505  omabs2  43951  iunconnlem2  45535  modelaxrep  45582  suplesup  45947  infleinflem2  45978  xrralrecnnle  45990  rexabslelem  46024  limcrecl  46237  limcleqr  46250  0ellimcdiv  46255  limclner  46257  limsupubuz  46319  limsupvaluz2  46344  supcnvlimsup  46346  climxrre  46356  xlimmnfvlem2  46439  xlimmnfv  46440  xlimpnfvlem2  46443  xlimpnfv  46444  icccncfext  46493  ioodvbdlimc1lem2  46538  ioodvbdlimc2lem  46540  fourierdlem50  46762  fourierdlem51  46763  fourierdlem80  46792  fourierdlem87  46799  fourierdlem103  46815  fourierdlem104  46816  meaiuninc3v  47090  omef  47102  smflimlem2  47378  smflimlem4  47380  smfmullem3  47399  fsupdm  47448  finfdm  47452  chnerlem1  47490  imaf1co  49818  upfval  49839  fuco21  49999  prcofvalg  50039