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  8142  tfrlem1  8398  injresinj  13809  swrdccatin1  14745  reuccatpfxs1  14767  prdsval  17471  catcocl  17699  catass  17700  catpropd  17723  cidpropd  17724  monpropd  17752  subccocl  17861  funcco  17887  funcpropd  17918  fucpropd  17996  initoeu2lem1  18030  xpcpropd  18223  curf2ndf  18262  drsdirfi  18321  mhmmnd  19051  ghmqusnsg  19269  ghmquskerlem3  19273  gsmsymgreqlem2  19417  dfod2  19550  ghmcmn  19817  rhmqusnsg  21257  psgndif  21574  dmatscmcl  22457  smatvscl  22478  cpmatmcllem  22672  pm2mpmhmlem2  22773  chfacfscmulgsum  22814  chfacfpmmulgsum  22818  neitr  23134  1stcrest  23407  dissnref  23482  dissnlocfin  23483  neitx  23561  tgqtop  23666  ptcmplem3  24008  trust  24184  utoptop  24189  restutopopn  24193  ustuqtop2  24197  ustuqtop4  24199  utop3cls  24206  met1stc  24478  prdsxmslem2  24486  metustexhalf  24513  cfilucfil  24516  metucn  24528  aannenlem1  26306  ulmuni  26371  lgamucov  27017  2sqmo  27417  pntpbnd  27568  pntlem3  27589  noetasuplem4  27717  noetainflem4  27721  tgbtwndiff  28450  tgifscgr  28452  iscgrglt  28458  tgbtwnconn1lem3  28518  tgbtwnconn1  28519  legov  28529  legtrd  28533  legtri3  28534  ltgseg  28540  legso  28543  tglinethru  28580  tglnpt2  28585  colline  28593  miriso  28614  midexlem  28636  perpneq  28658  isperp2  28659  footexALT  28662  footex  28665  midex  28681  opphllem3  28693  opphl  28698  hlpasch  28700  lnopp2hpgb  28707  lmieu  28728  trgcopyeu  28750  dfcgra2  28774  f1otrg  28815  axcontlem2  28910  2pthon3v  29891  2ndresdju  32594  fnpreimac  32616  fsumiunle  32771  ressprs  32893  dfmgc2  32925  mgcf1o  32932  chnind  32940  chnub  32941  chnso  32943  mndlrinvb  32969  mndlactf1o  32974  gsumfs2d  32997  gsumwun  33007  gsumwrd2dccatlem  33008  omndmul2  33028  tocyccntz  33103  cyc3genpm  33111  cycpmconjs  33115  cyc3conja  33116  isarchi3  33133  elrgspnlem4  33188  erler  33208  elrlocbasi  33209  rlocaddval  33211  rlocmulval  33212  rloccring  33213  rlocf1  33216  isdrng4  33237  fracfld  33250  isarchiofld  33287  imaslmod  33316  dvdsruasso  33348  nsgqusf1olem1  33376  nsgqusf1olem3  33378  lmhmqusker  33380  intlidl  33383  rhmquskerlem  33388  elrspunidl  33391  elrspunsn  33392  idlinsubrg  33394  rhmimaidl  33395  drngidl  33396  isprmidlc  33410  rhmpreimaprmidl  33414  qsidomlem2  33416  ssdifidllem  33419  ssdifidlprm  33421  mxidlprm  33433  mxidlirredi  33434  ssmxidllem  33436  ssmxidl  33437  opprqusplusg  33452  opprqusmulr  33454  qsdrngi  33458  qsdrng  33460  rsprprmprmidlb  33486  rprmdvdsprod  33497  1arithidom  33500  1arithufdlem2  33508  1arithufdlem3  33509  dfufd2lem  33512  r1plmhm  33565  r1pquslmic  33566  lbsdiflsp0  33612  dimkerim  33613  fedgmul  33617  fldextrspunlsplem  33660  constrconj  33725  constrfin  33726  constrelextdg2  33727  constrextdg2lem  33728  constrfiss  33731  ist0cld  33791  txomap  33792  qtophaus  33794  zarcls1  33827  zarclsint  33830  zarclssn  33831  pstmxmet  33855  sqsscirc1  33866  lmxrge0  33910  esumcst  34023  esumfsup  34030  esum2dlem  34052  esum2d  34053  esumiun  34054  ldsysgenld  34120  sigapildsys  34122  omssubadd  34261  signstfvneq0  34546  actfunsnf1o  34578  afsval  34645  nn0prpwlem  36282  lindsenlbs  37581  matunitlindflem1  37582  matunitlindflem2  37583  mblfinlem3  37625  itg2addnclem  37637  sstotbnd2  37740  prdstotbnd  37760  lcfl8  41463  fldhmf1  42050  mndmolinv  42055  primrootscoprmpow  42059  primrootspoweq0  42066  aks6d1c2p2  42079  aks6d1c2lem4  42087  aks6d1c2  42090  aks6d1c5  42099  aks6d1c6lem3  42132  unitscyglem3  42157  fiabv  42509  dffltz  42607  flt4lem7  42632  nna4b4nsq  42633  diophren  42787  rencldnfilem  42794  pellex  42809  pell1234qrdich  42835  pell1qrgap  42848  pellfundex  42860  omabs2  43307  iunconnlem2  44912  modelaxrep  44955  suplesup  45307  infleinflem2  45339  xrralrecnnle  45351  rexabslelem  45386  limcrecl  45601  limcleqr  45616  0ellimcdiv  45621  limclner  45623  limsupubuz  45685  limsupvaluz2  45710  supcnvlimsup  45712  climxrre  45722  xlimmnfvlem2  45805  xlimmnfv  45806  xlimpnfvlem2  45809  xlimpnfv  45810  icccncfext  45859  ioodvbdlimc1lem2  45904  ioodvbdlimc2lem  45906  fourierdlem50  46128  fourierdlem51  46129  fourierdlem80  46158  fourierdlem87  46165  fourierdlem103  46181  fourierdlem104  46182  meaiuninc3v  46456  omef  46468  smflimlem2  46744  smflimlem4  46746  smfmullem3  46765  fsupdm  46814  finfdm  46818  upfval  48904  fuco21  49007