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 732	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  8176  tfrlem1  8432  injresinj  13838  swrdccatin1  14773  reuccatpfxs1  14795  prdsval  17515  catcocl  17743  catass  17744  catpropd  17767  cidpropd  17768  monpropd  17798  subccocl  17909  funcco  17935  funcpropd  17967  fucpropd  18047  initoeu2lem1  18081  xpcpropd  18278  curf2ndf  18317  drsdirfi  18375  mhmmnd  19104  ghmqusnsg  19322  ghmquskerlem3  19326  gsmsymgreqlem2  19473  dfod2  19606  ghmcmn  19873  rhmqusnsg  21318  psgndif  21643  dmatscmcl  22530  smatvscl  22551  cpmatmcllem  22745  pm2mpmhmlem2  22846  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  neitr  23209  1stcrest  23482  dissnref  23557  dissnlocfin  23558  neitx  23636  tgqtop  23741  ptcmplem3  24083  trust  24259  utoptop  24264  restutopopn  24268  ustuqtop2  24272  ustuqtop4  24274  utop3cls  24281  met1stc  24555  prdsxmslem2  24563  metustexhalf  24590  cfilucfil  24593  metucn  24605  aannenlem1  26388  ulmuni  26453  lgamucov  27099  2sqmo  27499  pntpbnd  27650  pntlem3  27671  noetasuplem4  27799  noetainflem4  27803  tgbtwndiff  28532  tgifscgr  28534  iscgrglt  28540  tgbtwnconn1lem3  28600  tgbtwnconn1  28601  legov  28611  legtrd  28615  legtri3  28616  ltgseg  28622  legso  28625  tglinethru  28662  tglnpt2  28667  colline  28675  miriso  28696  midexlem  28718  perpneq  28740  isperp2  28741  footexALT  28744  footex  28747  midex  28763  opphllem3  28775  opphl  28780  hlpasch  28782  lnopp2hpgb  28789  lmieu  28810  trgcopyeu  28832  dfcgra2  28856  f1otrg  28897  axcontlem2  28998  2pthon3v  29976  2ndresdju  32667  fnpreimac  32689  fsumiunle  32833  ressprs  32936  dfmgc2  32969  mgcf1o  32976  chnind  32983  chnub  32984  chnso  32986  mndlrinvb  33011  mndlactf1o  33016  omndmul2  33062  tocyccntz  33137  cyc3genpm  33145  cycpmconjs  33149  cyc3conja  33150  isarchi3  33167  erler  33237  elrlocbasi  33238  rlocaddval  33240  rlocmulval  33241  rloccring  33242  rlocf1  33245  isdrng4  33264  fracfld  33275  isarchiofld  33312  imaslmod  33346  dvdsruasso  33378  nsgqusf1olem1  33406  nsgqusf1olem3  33408  lmhmqusker  33410  intlidl  33413  rhmquskerlem  33418  elrspunidl  33421  elrspunsn  33422  idlinsubrg  33424  rhmimaidl  33425  drngidl  33426  isprmidlc  33440  rhmpreimaprmidl  33444  qsidomlem2  33446  ssdifidllem  33449  ssdifidlprm  33451  mxidlprm  33463  mxidlirredi  33464  ssmxidllem  33466  ssmxidl  33467  opprqusplusg  33482  opprqusmulr  33484  qsdrngi  33488  qsdrng  33490  rsprprmprmidlb  33516  rprmdvdsprod  33527  1arithidom  33530  1arithufdlem2  33538  1arithufdlem3  33539  dfufd2lem  33542  r1plmhm  33595  r1pquslmic  33596  lbsdiflsp0  33639  dimkerim  33640  fedgmul  33644  constrconj  33735  constrfin  33736  constrelextdg2  33737  ist0cld  33779  txomap  33780  qtophaus  33782  zarcls1  33815  zarclsint  33818  zarclssn  33819  pstmxmet  33843  sqsscirc1  33854  lmxrge0  33898  esumcst  34027  esumfsup  34034  esum2dlem  34056  esum2d  34057  esumiun  34058  ldsysgenld  34124  sigapildsys  34126  omssubadd  34265  signstfvneq0  34549  actfunsnf1o  34581  afsval  34648  nn0prpwlem  36288  lindsenlbs  37575  matunitlindflem1  37576  matunitlindflem2  37577  mblfinlem3  37619  itg2addnclem  37631  sstotbnd2  37734  prdstotbnd  37754  lcfl8  41459  fldhmf1  42047  mndmolinv  42052  primrootscoprmpow  42056  primrootspoweq0  42063  aks6d1c2p2  42076  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c5  42096  aks6d1c6lem3  42129  unitscyglem3  42154  fiabv  42491  dffltz  42589  flt4lem7  42614  nna4b4nsq  42615  diophren  42769  rencldnfilem  42776  pellex  42791  pell1234qrdich  42817  pell1qrgap  42830  pellfundex  42842  omabs2  43294  iunconnlem2  44906  suplesup  45254  infleinflem2  45286  xrralrecnnle  45298  rexabslelem  45333  limcrecl  45550  limcleqr  45565  0ellimcdiv  45570  limclner  45572  limsupubuz  45634  limsupvaluz2  45659  supcnvlimsup  45661  climxrre  45671  xlimmnfvlem2  45754  xlimmnfv  45755  xlimpnfvlem2  45758  xlimpnfv  45759  icccncfext  45808  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  fourierdlem50  46077  fourierdlem51  46078  fourierdlem80  46107  fourierdlem87  46114  fourierdlem103  46130  fourierdlem104  46131  meaiuninc3v  46405  omef  46417  smflimlem2  46693  smflimlem4  46695  smfmullem3  46714  fsupdm  46763  finfdm  46767