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  8114  tfrlem1  8344  injresinj  13749  swrdccatin1  14690  reuccatpfxs1  14712  prdsval  17418  catcocl  17646  catass  17647  catpropd  17670  cidpropd  17671  monpropd  17699  subccocl  17807  funcco  17833  funcpropd  17864  fucpropd  17942  initoeu2lem1  17976  xpcpropd  18169  curf2ndf  18208  drsdirfi  18266  mhmmnd  18996  ghmqusnsg  19214  ghmquskerlem3  19218  gsmsymgreqlem2  19361  dfod2  19494  ghmcmn  19761  rhmqusnsg  21195  psgndif  21511  dmatscmcl  22390  smatvscl  22411  cpmatmcllem  22605  pm2mpmhmlem2  22706  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  neitr  23067  1stcrest  23340  dissnref  23415  dissnlocfin  23416  neitx  23494  tgqtop  23599  ptcmplem3  23941  trust  24117  utoptop  24122  restutopopn  24126  ustuqtop2  24130  ustuqtop4  24132  utop3cls  24139  met1stc  24409  prdsxmslem2  24417  metustexhalf  24444  cfilucfil  24447  metucn  24459  aannenlem1  26236  ulmuni  26301  lgamucov  26948  2sqmo  27348  pntpbnd  27499  pntlem3  27520  noetasuplem4  27648  noetainflem4  27652  tgbtwndiff  28433  tgifscgr  28435  iscgrglt  28441  tgbtwnconn1lem3  28501  tgbtwnconn1  28502  legov  28512  legtrd  28516  legtri3  28517  ltgseg  28523  legso  28526  tglinethru  28563  tglnpt2  28568  colline  28576  miriso  28597  midexlem  28619  perpneq  28641  isperp2  28642  footexALT  28645  footex  28648  midex  28664  opphllem3  28676  opphl  28681  hlpasch  28683  lnopp2hpgb  28690  lmieu  28711  trgcopyeu  28733  dfcgra2  28757  f1otrg  28798  axcontlem2  28892  2pthon3v  29873  2ndresdju  32573  fnpreimac  32595  fsumiunle  32754  ressprs  32890  dfmgc2  32922  mgcf1o  32929  chnind  32937  chnub  32938  chnso  32940  mndlrinvb  32966  mndlactf1o  32971  gsumfs2d  32995  gsumwun  33005  gsumwrd2dccatlem  33006  omndmul2  33026  tocyccntz  33101  cyc3genpm  33109  cycpmconjs  33113  cyc3conja  33114  isarchi3  33141  elrgspnlem4  33196  erler  33216  elrlocbasi  33217  rlocaddval  33219  rlocmulval  33220  rloccring  33221  rlocf1  33224  isdrng4  33245  fracfld  33258  isarchiofld  33295  imaslmod  33324  dvdsruasso  33356  nsgqusf1olem1  33384  nsgqusf1olem3  33386  lmhmqusker  33388  intlidl  33391  rhmquskerlem  33396  elrspunidl  33399  elrspunsn  33400  idlinsubrg  33402  rhmimaidl  33403  drngidl  33404  isprmidlc  33418  rhmpreimaprmidl  33422  qsidomlem2  33424  ssdifidllem  33427  ssdifidlprm  33429  mxidlprm  33441  mxidlirredi  33442  ssmxidllem  33444  ssmxidl  33445  opprqusplusg  33460  opprqusmulr  33462  qsdrngi  33466  qsdrng  33468  rsprprmprmidlb  33494  rprmdvdsprod  33505  1arithidom  33508  1arithufdlem2  33516  1arithufdlem3  33517  dfufd2lem  33520  r1plmhm  33575  r1pquslmic  33576  lbsdiflsp0  33622  dimkerim  33623  fedgmul  33627  fldextrspunlsplem  33668  constrconj  33735  constrfin  33736  constrelextdg2  33737  constrextdg2lem  33738  constrfiss  33741  ist0cld  33823  txomap  33824  qtophaus  33826  zarcls1  33859  zarclsint  33862  zarclssn  33863  pstmxmet  33887  sqsscirc1  33898  lmxrge0  33942  esumcst  34053  esumfsup  34060  esum2dlem  34082  esum2d  34083  esumiun  34084  ldsysgenld  34150  sigapildsys  34152  omssubadd  34291  signstfvneq0  34563  actfunsnf1o  34595  afsval  34662  nn0prpwlem  36310  lindsenlbs  37609  matunitlindflem1  37610  matunitlindflem2  37611  mblfinlem3  37653  itg2addnclem  37665  sstotbnd2  37768  prdstotbnd  37788  lcfl8  41496  fldhmf1  42078  mndmolinv  42083  primrootscoprmpow  42087  primrootspoweq0  42094  aks6d1c2p2  42107  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c5  42127  aks6d1c6lem3  42160  unitscyglem3  42185  fiabv  42524  dffltz  42622  flt4lem7  42647  nna4b4nsq  42648  diophren  42801  rencldnfilem  42808  pellex  42823  pell1234qrdich  42849  pell1qrgap  42862  pellfundex  42874  omabs2  43321  iunconnlem2  44924  modelaxrep  44971  suplesup  45335  infleinflem2  45367  xrralrecnnle  45379  rexabslelem  45414  limcrecl  45627  limcleqr  45642  0ellimcdiv  45647  limclner  45649  limsupubuz  45711  limsupvaluz2  45736  supcnvlimsup  45738  climxrre  45748  xlimmnfvlem2  45831  xlimmnfv  45832  xlimpnfvlem2  45835  xlimpnfv  45836  icccncfext  45885  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  fourierdlem50  46154  fourierdlem51  46155  fourierdlem80  46184  fourierdlem87  46191  fourierdlem103  46207  fourierdlem104  46208  meaiuninc3v  46482  omef  46494  smflimlem2  46770  smflimlem4  46772  smfmullem3  46791  fsupdm  46840  finfdm  46844  imaf1co  49144  upfval  49165  fuco21  49325  prcofvalg  49365