Theorem simp-4r 796

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 746	1 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fimaproj  8179  tfrlem1  8411  injresinj  13953  swrdccatin1  14902  reuccatpfxs1  14924  prdsval  17655  catcocl  17888  catass  17889  catpropd  17912  cidpropd  17913  monpropd  17941  subccocl  18049  funcco  18075  funcpropd  18106  fucpropd  18184  initoeu2lem1  18218  xpcpropd  18411  curf2ndf  18450  drsdirfi  18508  chnind  18824  chnub  18825  chnso  18827  mhmmnd  19303  ghmqusnsg  19526  ghmquskerlem3  19530  gsmsymgreqlem2  19675  dfod2  19808  ghmcmn  20075  omndmul2  20377  isdrng4  21022  drngidl  21569  rhmqusnsg  21611  isprmidlc  21658  rhmpreimaprmidl  21665  qsidomlem2  21667  ssdifidllem  21670  ssdifidlprm  21672  psgndif  21938  lindsenlbs  22187  dmatscmcl  22848  smatvscl  22869  matunitlindflem1  23024  matunitlindflem2  23025  cpmatmcllem  23066  pm2mpmhmlem2  23167  chfacfscmulgsum  23208  chfacfpmmulgsum  23212  neitr  23528  1stcrest  23801  dissnref  23877  dissnlocfin  23878  neitx  23956  tgqtop  24061  ptcmplem3  24403  trust  24578  utoptop  24583  restutopopn  24587  ustuqtop2  24591  ustuqtop4  24593  utop3cls  24600  met1stc  24870  prdsxmslem2  24878  metustexhalf  24905  cfilucfil  24908  metucn  24920  aannenlem1  26685  ulmuni  26749  lgamucov  27395  2sqmo  27794  pntpbnd  27945  pntlem3  27966  flt4lem7  28019  noetasuplem4  28123  noetainflem4  28127  bdayfinbndlem1  28883  tgsegconeu  28979  tgbtwndiff  28999  tgifscgr  29001  iscgrglt  29007  tgbtwnconn1lem3  29067  tgbtwnconn1  29068  legov  29078  legtrd  29082  legtri3  29083  ltgseg  29089  legso  29092  tglinethru  29134  tglinesseq  29138  colline  29148  tglnpt2  29151  tglnpt4  29153  miriso  29172  midexlem  29194  perpneq  29219  isperp2  29220  footexALT  29223  footex  29226  midex  29243  opphllem3  29255  opphl  29260  hlpasch  29264  lnopp2hpgb  29271  plngcplem  29293  lnssplng  29300  plng3p  29305  lmieu  29319  trgcopyeu  29343  zerocgra  29361  dfcgra2  29368  ragcgra  29373  cgrarag  29374  ragsupplcgra  29375  tgaaddcpbllem1  29379  cgraer  29407  cgrabasimass  29408  angmgmaddeu1  29409  angmgmaddeu2  29410  angmgmaddeu3  29411  angmgmaddcpbl  29420  angmgmaddcl  29421  angmgmaddlid  29422  angmgmaddrid  29423  prlnghpg  29454  dfprlng2  29455  dfprlng3  29456  perpprlng  29458  prlngex  29459  prlngmolem1  29460  prlngmolem2  29461  quadcgrprlng  29474  f1otrg  29478  axcontlem2  29573  2pthon3v  30562  2ndresdju  33315  fnpreimac  33336  fsumiunle  33490  ressprs  33597  dfmgc2  33627  mgcf1o  33634  mndlrinvb  33656  mndlactf1o  33661  gsumfs2d  33692  gsumwun  33707  gsumwrd2dccatlem  33708  tocyccntz  33775  cyc3genpm  33783  cycpmconjs  33787  cyc3conja  33788  isarchi3  33818  isarchiofld  33830  elrgspnlem4  33876  erler  33896  elrlocbasi  33898  rlocaddval  33900  rlocmulval  33901  rloccring  33902  rlocf1  33905  rlocisunit  33907  ricdomn1  33920  fracfld  33940  imaslmod  33984  dvdsruasso  34010  nsgqusf1olem1  34034  nsgqusf1olem3  34036  lmhmqusker  34038  intlidl  34040  rhmquskerlem  34045  elrspunidl  34048  elrspunsn  34049  idlinsubrg  34051  rhmimaidl  34052  mxidlprm  34065  mxidlirredi  34066  ssmxidllem  34068  ssmxidl  34069  opprqusplusg  34083  opprqusmulr  34085  qsdrngi  34089  qsdrng  34091  drnglring  34094  dflring2  34095  dflringlem3  34098  dflring4  34100  rsprprmprmidlb  34125  rprmdvdsprod  34136  1arithidom  34139  1arithufdlem2  34147  1arithufdlem3  34148  dfufd2lem  34151  r1plmhm  34211  r1pquslmic  34212  mplidomlem  34229  lbsdiflsp0  34328  dimkerim  34329  fedgmul  34333  fldextrspunlsplem  34375  extdgfialg  34396  constrconj  34447  constrfin  34448  constrelextdg2  34449  constrextdg2lem  34450  constrfiss  34453  ist0cld  34535  txomap  34536  qtophaus  34538  zarcls1  34571  zarclsint  34574  zarclssn  34575  pstmxmet  34599  sqsscirc1  34610  lmxrge0  34654  esumcst  34765  esumfsup  34772  esum2dlem  34794  esum2d  34795  esumiun  34796  ldsysgenld  34863  sigapildsys  34865  omssubadd  35002  signstfvneq0  35271  actfunsnf1o  35303  afsval  35373  nn0prpwlem  37288  mh-inf3f1  37507  mblfinlem3  38769  itg2addnclem  38781  sstotbnd2  38900  prdstotbnd  38920  lcfl8  42751  fldhmf1  43332  mndmolinv  43337  primrootscoprmpow  43341  primrootspoweq0  43348  aks6d1c2p2  43361  aks6d1c2lem4  43369  aks6d1c2  43372  aks6d1c5  43381  aks6d1c6lem3  43414  unitscyglem3  43439  fiabv  43793  dffltz  43863  diophren  44013  rencldnfilem  44020  pellex  44035  pell1234qrdich  44061  pell1qrgap  44074  pellfundex  44086  omabs2  44526  iunconnlem2  46108  modelaxrep  46166  suplesup  46556  infleinflem2  46587  xrralrecnnle  46599  rexabslelem  46633  limcrecl  46846  limcleqr  46859  0ellimcdiv  46864  limclner  46866  limsupubuz  46928  limsupvaluz2  46953  supcnvlimsup  46955  climxrre  46965  xlimmnfvlem2  47048  xlimmnfv  47049  xlimpnfvlem2  47052  xlimpnfv  47053  icccncfext  47102  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  fourierdlem50  47371  fourierdlem51  47372  fourierdlem80  47401  fourierdlem87  47408  fourierdlem103  47424  fourierdlem104  47425  meaiuninc3v  47699  omef  47711  smflimlem2  47987  smflimlem4  47989  smfmullem3  48008  fsupdm  48057  finfdm  48061  chnerlem1  48097  imaf1co  50476  upfval  50497  fuco21  50663  prcofvalg  50716