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  8158  tfrlem1  8414  injresinj  13823  swrdccatin1  14759  reuccatpfxs1  14781  prdsval  17501  catcocl  17729  catass  17730  catpropd  17753  cidpropd  17754  monpropd  17784  subccocl  17895  funcco  17921  funcpropd  17953  fucpropd  18033  initoeu2lem1  18067  xpcpropd  18264  curf2ndf  18303  drsdirfi  18362  mhmmnd  19094  ghmqusnsg  19312  ghmquskerlem3  19316  gsmsymgreqlem2  19463  dfod2  19596  ghmcmn  19863  rhmqusnsg  21312  psgndif  21637  dmatscmcl  22524  smatvscl  22545  cpmatmcllem  22739  pm2mpmhmlem2  22840  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  neitr  23203  1stcrest  23476  dissnref  23551  dissnlocfin  23552  neitx  23630  tgqtop  23735  ptcmplem3  24077  trust  24253  utoptop  24258  restutopopn  24262  ustuqtop2  24266  ustuqtop4  24268  utop3cls  24275  met1stc  24549  prdsxmslem2  24557  metustexhalf  24584  cfilucfil  24587  metucn  24599  aannenlem1  26384  ulmuni  26449  lgamucov  27095  2sqmo  27495  pntpbnd  27646  pntlem3  27667  noetasuplem4  27795  noetainflem4  27799  tgbtwndiff  28528  tgifscgr  28530  iscgrglt  28536  tgbtwnconn1lem3  28596  tgbtwnconn1  28597  legov  28607  legtrd  28611  legtri3  28612  ltgseg  28618  legso  28621  tglinethru  28658  tglnpt2  28663  colline  28671  miriso  28692  midexlem  28714  perpneq  28736  isperp2  28737  footexALT  28740  footex  28743  midex  28759  opphllem3  28771  opphl  28776  hlpasch  28778  lnopp2hpgb  28785  lmieu  28806  trgcopyeu  28828  dfcgra2  28852  f1otrg  28893  axcontlem2  28994  2pthon3v  29972  2ndresdju  32665  fnpreimac  32687  fsumiunle  32835  ressprs  32938  dfmgc2  32970  mgcf1o  32977  chnind  32984  chnub  32985  chnso  32987  mndlrinvb  33012  mndlactf1o  33017  gsumfs2d  33040  gsumwun  33050  gsumwrd2dccatlem  33051  omndmul2  33071  tocyccntz  33146  cyc3genpm  33154  cycpmconjs  33158  cyc3conja  33159  isarchi3  33176  elrgspnlem4  33234  erler  33251  elrlocbasi  33252  rlocaddval  33254  rlocmulval  33255  rloccring  33256  rlocf1  33259  isdrng4  33278  fracfld  33289  isarchiofld  33326  imaslmod  33360  dvdsruasso  33392  nsgqusf1olem1  33420  nsgqusf1olem3  33422  lmhmqusker  33424  intlidl  33427  rhmquskerlem  33432  elrspunidl  33435  elrspunsn  33436  idlinsubrg  33438  rhmimaidl  33439  drngidl  33440  isprmidlc  33454  rhmpreimaprmidl  33458  qsidomlem2  33460  ssdifidllem  33463  ssdifidlprm  33465  mxidlprm  33477  mxidlirredi  33478  ssmxidllem  33480  ssmxidl  33481  opprqusplusg  33496  opprqusmulr  33498  qsdrngi  33502  qsdrng  33504  rsprprmprmidlb  33530  rprmdvdsprod  33541  1arithidom  33544  1arithufdlem2  33552  1arithufdlem3  33553  dfufd2lem  33556  r1plmhm  33609  r1pquslmic  33610  lbsdiflsp0  33653  dimkerim  33654  fedgmul  33658  constrconj  33749  constrfin  33750  constrelextdg2  33751  ist0cld  33793  txomap  33794  qtophaus  33796  zarcls1  33829  zarclsint  33832  zarclssn  33833  pstmxmet  33857  sqsscirc1  33868  lmxrge0  33912  esumcst  34043  esumfsup  34050  esum2dlem  34072  esum2d  34073  esumiun  34074  ldsysgenld  34140  sigapildsys  34142  omssubadd  34281  signstfvneq0  34565  actfunsnf1o  34597  afsval  34664  nn0prpwlem  36304  lindsenlbs  37601  matunitlindflem1  37602  matunitlindflem2  37603  mblfinlem3  37645  itg2addnclem  37657  sstotbnd2  37760  prdstotbnd  37780  lcfl8  41484  fldhmf1  42071  mndmolinv  42076  primrootscoprmpow  42080  primrootspoweq0  42087  aks6d1c2p2  42100  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c5  42120  aks6d1c6lem3  42153  unitscyglem3  42178  fiabv  42522  dffltz  42620  flt4lem7  42645  nna4b4nsq  42646  diophren  42800  rencldnfilem  42807  pellex  42822  pell1234qrdich  42848  pell1qrgap  42861  pellfundex  42873  omabs2  43321  iunconnlem2  44932  modelaxrep  44945  suplesup  45288  infleinflem2  45320  xrralrecnnle  45332  rexabslelem  45367  limcrecl  45584  limcleqr  45599  0ellimcdiv  45604  limclner  45606  limsupubuz  45668  limsupvaluz2  45693  supcnvlimsup  45695  climxrre  45705  xlimmnfvlem2  45788  xlimmnfv  45789  xlimpnfvlem2  45792  xlimpnfv  45793  icccncfext  45842  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  fourierdlem50  46111  fourierdlem51  46112  fourierdlem80  46141  fourierdlem87  46148  fourierdlem103  46164  fourierdlem104  46165  meaiuninc3v  46439  omef  46451  smflimlem2  46727  smflimlem4  46729  smfmullem3  46748  fsupdm  46797  finfdm  46801