Theorem simp-5r 798

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-5r	⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simp-5r

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad5antlr 748	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:  catcocl  17891  catass  17892  monpropd  17944  subccocl  18052  funcco  18078  funcpropd  18109  chnub  18828  mhmmnd  19306  ghmqusnsg  19529  ghmquskerlem3  19533  omndmul2  20380  rhmqusnsg  21614  rhmpreimaprmidl  21668  ssdifidllem  21673  ssdifidlprm  21675  matunitlindflem1  23027  pm2mpmhmlem2  23170  neitr  23531  restutopopn  24590  ustuqtop4  24596  utopreg  24604  cfilucfil  24911  psmetutop  24919  dyadmax  25952  2sqmo  27797  tgsegconeu  28982  tgifscgr  29004  tgcgrxfr  29014  tgbtwnconn1lem3  29070  tgbtwnconn1  29071  legov  29081  legtrd  29085  legso  29095  miriso  29175  perpneq  29222  footexALT  29226  footex  29229  colperpex  29242  opphllem  29244  midex  29246  opphl  29263  lnopp2hpgb  29274  trgcopyeu  29346  zerocgra  29364  dfcgra2  29371  ragcgra  29376  cgrarag  29377  ragsupplcgra  29378  tgaaddcpbllem1  29382  tgaaddcpbl  29385  inaghl  29397  cgraer  29410  cgrabasimass  29411  angmgmaddcpbl  29423  angmgmaddcl  29424  angmgmaddlid  29425  angmgmaddrid  29426  perpprlng  29461  prlngmolem1  29463  prlngmolem2  29464  prlngmo2  29467  f1otrg  29481  2ndresdju  33318  nn0xmulclb  33436  psgnfzto1stlem  33737  cyc3genpm  33789  elrgspnlem4  33882  rloccring  33908  rlocf1  33911  ricdomn1  33926  zzedom  33939  edompidlem  33940  dvdsruasso  34024  nsgqusf1olem3  34050  rhmquskerlem  34059  elrspunidl  34062  rhmimaidl  34066  mxidlprm  34079  mxidlirredi  34080  ssmxidl  34083  qsdrngi  34103  qsdrng  34105  1arithidom  34153  1arithufdlem3  34162  r1plmhm  34224  r1pquslmic  34225  mplidomlem  34242  vieta  34295  lbsdiflsp0  34341  fldext2chn  34443  constrconj  34460  constrfin  34461  constrelextdg2  34462  constrfiss  34466  cos9thpiminplylem2  34498  qtophaus  34551  locfinreflem  34555  cmpcref  34565  pstmxmet  34612  lmxrge0  34667  esumcst  34778  omssubadd  35015  signstfvneq0  35284  afsval  35386  heicant  38778  sstotbnd2  38911  primrootscoprmpow  43352  primrootspoweq0  43359  aks6d1c2p2  43372  aks6d1c2lem4  43380  aks6d1c2  43383  unitscyglem3  43450  dffltz  43874  eldioph2b  43978  diophren  44024  pell1234qrdich  44072  omabs2  44537  iunconnlem2  46119  limcrecl  46856  limclner  46876  icccncfext  47112  ioodvbdlimc1lem2  47157  ioodvbdlimc2lem  47159  stoweidlem60  47285  fourierdlem51  47382  fourierdlem77  47408  fourierdlem103  47434  fourierdlem104  47435  smfaddlem1  47988  smfmullem3  48018  chnerlem1  48107  grtriprop  49254  upfval  50507  fuco21  50673