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  8154  tfrlem1  8386  injresinj  13929  swrdccatin1  14878  reuccatpfxs1  14900  prdsval  17631  catcocl  17864  catass  17865  catpropd  17888  cidpropd  17889  monpropd  17917  subccocl  18025  funcco  18051  funcpropd  18082  fucpropd  18160  initoeu2lem1  18194  xpcpropd  18387  curf2ndf  18426  drsdirfi  18484  chnind  18800  chnub  18801  chnso  18803  mhmmnd  19279  ghmqusnsg  19501  ghmquskerlem3  19505  gsmsymgreqlem2  19650  dfod2  19783  ghmcmn  20050  omndmul2  20352  isdrng4  20997  drngidl  21544  rhmqusnsg  21586  isprmidlc  21633  rhmpreimaprmidl  21640  qsidomlem2  21642  ssdifidllem  21645  ssdifidlprm  21647  psgndif  21913  lindsenlbs  22162  dmatscmcl  22823  smatvscl  22844  matunitlindflem1  22999  matunitlindflem2  23000  cpmatmcllem  23041  pm2mpmhmlem2  23142  chfacfscmulgsum  23183  chfacfpmmulgsum  23187  neitr  23503  1stcrest  23776  dissnref  23852  dissnlocfin  23853  neitx  23931  tgqtop  24036  ptcmplem3  24378  trust  24553  utoptop  24558  restutopopn  24562  ustuqtop2  24566  ustuqtop4  24568  utop3cls  24575  met1stc  24845  prdsxmslem2  24853  metustexhalf  24880  cfilucfil  24883  metucn  24895  aannenlem1  26660  ulmuni  26724  lgamucov  27370  2sqmo  27769  pntpbnd  27920  pntlem3  27941  flt4lem7  27994  noetasuplem4  28098  noetainflem4  28102  bdayfinbndlem1  28858  tgsegconeu  28954  tgbtwndiff  28974  tgifscgr  28976  iscgrglt  28982  tgbtwnconn1lem3  29042  tgbtwnconn1  29043  legov  29053  legtrd  29057  legtri3  29058  ltgseg  29064  legso  29067  tglinethru  29109  tglinesseq  29113  colline  29123  tglnpt2  29126  tglnpt4  29128  miriso  29147  midexlem  29169  perpneq  29194  isperp2  29195  footexALT  29198  footex  29201  midex  29218  opphllem3  29230  opphl  29235  hlpasch  29239  lnopp2hpgb  29246  plngcplem  29268  lnssplng  29275  plng3p  29280  lmieu  29294  trgcopyeu  29318  zerocgra  29336  dfcgra2  29343  ragcgra  29348  cgrarag  29349  ragsupplcgra  29350  tgaaddcpbllem1  29354  cgraer  29382  cgrabasimass  29383  angmgmaddeu1  29384  angmgmaddeu2  29385  angmgmaddeu3  29386  angmgmaddcpbl  29395  angmgmaddcl  29396  angmgmaddlid  29397  angmgmaddrid  29398  prlnghpg  29429  dfprlng2  29430  dfprlng3  29431  perpprlng  29433  prlngex  29434  prlngmolem1  29435  prlngmolem2  29436  quadcgrprlng  29449  f1otrg  29453  axcontlem2  29548  2pthon3v  30537  2ndresdju  33290  fnpreimac  33311  fsumiunle  33466  ressprs  33573  dfmgc2  33603  mgcf1o  33610  mndlrinvb  33632  mndlactf1o  33637  gsumfs2d  33668  gsumwun  33683  gsumwrd2dccatlem  33684  tocyccntz  33751  cyc3genpm  33759  cycpmconjs  33763  cyc3conja  33764  isarchi3  33794  isarchiofld  33806  elrgspnlem4  33852  erler  33872  elrlocbasi  33874  rlocaddval  33876  rlocmulval  33877  rloccring  33878  rlocf1  33881  rlocisunit  33883  ricdomn1  33896  fracfld  33916  imaslmod  33960  dvdsruasso  33986  nsgqusf1olem1  34010  nsgqusf1olem3  34012  lmhmqusker  34014  intlidl  34016  rhmquskerlem  34021  elrspunidl  34024  elrspunsn  34025  idlinsubrg  34027  rhmimaidl  34028  mxidlprm  34041  mxidlirredi  34042  ssmxidllem  34044  ssmxidl  34045  opprqusplusg  34059  opprqusmulr  34061  qsdrngi  34065  qsdrng  34067  drnglring  34070  dflring2  34071  dflringlem3  34074  dflring4  34076  rsprprmprmidlb  34101  rprmdvdsprod  34112  1arithidom  34115  1arithufdlem2  34123  1arithufdlem3  34124  dfufd2lem  34127  r1plmhm  34187  r1pquslmic  34188  mplidomlem  34205  lbsdiflsp0  34304  dimkerim  34305  fedgmul  34309  fldextrspunlsplem  34351  extdgfialg  34372  constrconj  34423  constrfin  34424  constrelextdg2  34425  constrextdg2lem  34426  constrfiss  34429  ist0cld  34511  txomap  34512  qtophaus  34514  zarcls1  34547  zarclsint  34550  zarclssn  34551  pstmxmet  34575  sqsscirc1  34586  lmxrge0  34630  esumcst  34741  esumfsup  34748  esum2dlem  34770  esum2d  34771  esumiun  34772  ldsysgenld  34839  sigapildsys  34841  omssubadd  34978  signstfvneq0  35247  actfunsnf1o  35279  afsval  35349  nn0prpwlem  37202  mh-inf3f1  37421  mblfinlem3  38670  itg2addnclem  38682  sstotbnd2  38801  prdstotbnd  38821  lcfl8  42652  fldhmf1  43233  mndmolinv  43238  primrootscoprmpow  43242  primrootspoweq0  43249  aks6d1c2p2  43262  aks6d1c2lem4  43270  aks6d1c2  43273  aks6d1c5  43282  aks6d1c6lem3  43315  unitscyglem3  43340  fiabv  43693  dffltz  43763  diophren  43913  rencldnfilem  43920  pellex  43935  pell1234qrdich  43961  pell1qrgap  43974  pellfundex  43986  omabs2  44427  iunconnlem2  46010  modelaxrep  46064  suplesup  46444  infleinflem2  46475  xrralrecnnle  46487  rexabslelem  46521  limcrecl  46734  limcleqr  46747  0ellimcdiv  46752  limclner  46754  limsupubuz  46816  limsupvaluz2  46841  supcnvlimsup  46843  climxrre  46853  xlimmnfvlem2  46936  xlimmnfv  46937  xlimpnfvlem2  46940  xlimpnfv  46941  icccncfext  46990  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  fourierdlem50  47259  fourierdlem51  47260  fourierdlem80  47289  fourierdlem87  47296  fourierdlem103  47312  fourierdlem104  47313  meaiuninc3v  47587  omef  47599  smflimlem2  47875  smflimlem4  47877  smfmullem3  47896  fsupdm  47945  finfdm  47949  chnerlem1  47985  imaf1co  50364  upfval  50385  fuco21  50551  prcofvalg  50604