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  8136  tfrlem1  8367  injresinj  13906  swrdccatin1  14854  reuccatpfxs1  14876  prdsval  17606  catcocl  17839  catass  17840  catpropd  17863  cidpropd  17864  monpropd  17892  subccocl  18000  funcco  18026  funcpropd  18057  fucpropd  18135  initoeu2lem1  18169  xpcpropd  18362  curf2ndf  18401  drsdirfi  18459  chnind  18775  chnub  18776  chnso  18778  mhmmnd  19254  ghmqusnsg  19476  ghmquskerlem3  19480  gsmsymgreqlem2  19625  dfod2  19758  ghmcmn  20025  omndmul2  20327  isdrng4  20972  drngidl  21519  rhmqusnsg  21561  isprmidlc  21608  rhmpreimaprmidl  21615  qsidomlem2  21617  ssdifidllem  21620  ssdifidlprm  21622  psgndif  21888  lindsenlbs  22137  dmatscmcl  22798  smatvscl  22819  matunitlindflem1  22974  matunitlindflem2  22975  cpmatmcllem  23016  pm2mpmhmlem2  23117  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  neitr  23478  1stcrest  23751  dissnref  23827  dissnlocfin  23828  neitx  23906  tgqtop  24011  ptcmplem3  24353  trust  24528  utoptop  24533  restutopopn  24537  ustuqtop2  24541  ustuqtop4  24543  utop3cls  24550  met1stc  24820  prdsxmslem2  24828  metustexhalf  24855  cfilucfil  24858  metucn  24870  aannenlem1  26637  ulmuni  26701  lgamucov  27347  2sqmo  27746  pntpbnd  27897  pntlem3  27918  flt4lem7  27971  nna4b4nsq  27972  noetasuplem4  28075  noetainflem4  28079  bdayfinbndlem1  28835  tgsegconeu  28931  tgbtwndiff  28951  tgifscgr  28953  iscgrglt  28959  tgbtwnconn1lem3  29019  tgbtwnconn1  29020  legov  29030  legtrd  29034  legtri3  29035  ltgseg  29041  legso  29044  tglinethru  29086  tglinesseq  29090  colline  29100  tglnpt2  29103  tglnpt4  29105  miriso  29124  midexlem  29146  perpneq  29171  isperp2  29172  footexALT  29175  footex  29178  midex  29195  opphllem3  29207  opphl  29212  hlpasch  29216  lnopp2hpgb  29223  plngcplem  29245  lnssplng  29252  plng3p  29257  lmieu  29271  trgcopyeu  29295  zerocgra  29313  dfcgra2  29320  ragcgra  29325  cgrarag  29326  ragsupplcgra  29327  tgaaddcpbllem1  29331  cgraer  29359  cgrabasimass  29360  angmgmaddeu1  29361  angmgmaddeu2  29362  angmgmaddeu3  29363  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmaddlid  29374  angmgmaddrid  29375  prlnghpg  29406  dfprlng2  29407  dfprlng3  29408  perpprlng  29410  prlngex  29411  prlngmolem1  29412  prlngmolem2  29413  quadcgrprlng  29426  f1otrg  29430  axcontlem2  29525  2pthon3v  30514  2ndresdju  33225  fnpreimac  33246  fsumiunle  33402  ressprs  33509  dfmgc2  33539  mgcf1o  33546  mndlrinvb  33568  mndlactf1o  33573  gsumfs2d  33604  gsumwun  33619  gsumwrd2dccatlem  33620  tocyccntz  33687  cyc3genpm  33695  cycpmconjs  33699  cyc3conja  33700  isarchi3  33730  isarchiofld  33742  elrgspnlem4  33788  erler  33808  elrlocbasi  33810  rlocaddval  33812  rlocmulval  33813  rloccring  33814  rlocf1  33817  rlocisunit  33819  ricdomn1  33832  fracfld  33852  imaslmod  33896  dvdsruasso  33922  nsgqusf1olem1  33946  nsgqusf1olem3  33948  lmhmqusker  33950  intlidl  33952  rhmquskerlem  33957  elrspunidl  33960  elrspunsn  33961  idlinsubrg  33963  rhmimaidl  33964  mxidlprm  33977  mxidlirredi  33978  ssmxidllem  33980  ssmxidl  33981  opprqusplusg  33995  opprqusmulr  33997  qsdrngi  34001  qsdrng  34003  drnglring  34006  dflring2  34007  dflringlem3  34010  dflring4  34012  rsprprmprmidlb  34037  rprmdvdsprod  34048  1arithidom  34051  1arithufdlem2  34059  1arithufdlem3  34060  dfufd2lem  34063  r1plmhm  34123  r1pquslmic  34124  mplidomlem  34141  lbsdiflsp0  34240  dimkerim  34241  fedgmul  34245  fldextrspunlsplem  34287  extdgfialg  34308  constrconj  34359  constrfin  34360  constrelextdg2  34361  constrextdg2lem  34362  constrfiss  34365  ist0cld  34447  txomap  34448  qtophaus  34450  zarcls1  34483  zarclsint  34486  zarclssn  34487  pstmxmet  34511  sqsscirc1  34522  lmxrge0  34566  esumcst  34677  esumfsup  34684  esum2dlem  34706  esum2d  34707  esumiun  34708  ldsysgenld  34775  sigapildsys  34777  omssubadd  34915  signstfvneq0  35184  actfunsnf1o  35216  afsval  35286  nn0prpwlem  37080  mh-inf3f1  37299  mblfinlem3  38545  itg2addnclem  38557  sstotbnd2  38676  prdstotbnd  38696  lcfl8  42527  fldhmf1  43108  mndmolinv  43113  primrootscoprmpow  43117  primrootspoweq0  43124  aks6d1c2p2  43137  aks6d1c2lem4  43145  aks6d1c2  43148  aks6d1c5  43157  aks6d1c6lem3  43190  unitscyglem3  43215  fiabv  43562  dffltz  43624  diophren  43773  rencldnfilem  43780  pellex  43795  pell1234qrdich  43821  pell1qrgap  43834  pellfundex  43846  omabs2  44292  iunconnlem2  45876  modelaxrep  45923  suplesup  46295  infleinflem2  46326  xrralrecnnle  46338  rexabslelem  46372  limcrecl  46585  limcleqr  46598  0ellimcdiv  46603  limclner  46605  limsupubuz  46667  limsupvaluz2  46692  supcnvlimsup  46694  climxrre  46704  xlimmnfvlem2  46787  xlimmnfv  46788  xlimpnfvlem2  46791  xlimpnfv  46792  icccncfext  46841  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  fourierdlem50  47110  fourierdlem51  47111  fourierdlem80  47140  fourierdlem87  47147  fourierdlem103  47163  fourierdlem104  47164  meaiuninc3v  47438  omef  47450  smflimlem2  47726  smflimlem4  47728  smfmullem3  47747  fsupdm  47796  finfdm  47800  chnerlem1  47836  imaf1co  50207  upfval  50228  fuco21  50388  prcofvalg  50428