Theorem simp-5r 797

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 747	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  catcocl  17731  catass  17732  monpropd  17784  subccocl  17892  funcco  17918  funcpropd  17949  chnub  18668  mhmmnd  19121  ghmqusnsg  19343  ghmquskerlem3  19347  omndmul2  20194  rhmqusnsg  21387  rhmpreimaprmidl  21439  ssdifidllem  21444  ssdifidlprm  21446  pm2mpmhmlem2  22937  neitr  23298  restutopopn  24356  ustuqtop4  24362  utopreg  24370  cfilucfil  24677  psmetutop  24685  dyadmax  25718  2sqmo  27559  tgifscgr  28735  tgcgrxfr  28745  tgbtwnconn1lem3  28801  tgbtwnconn1  28802  legov  28812  legtrd  28816  legso  28826  miriso  28901  perpneq  28945  footexALT  28949  footex  28952  colperpex  28964  opphllem  28966  midex  28968  opphl  28985  lnopp2hpgb  28994  trgcopyeu  29058  dfcgra2  29082  inaghl  29097  f1otrg  29129  2ndresdju  32906  nn0xmulclb  33028  psgnfzto1stlem  33333  cyc3genpm  33385  elrgspnlem4  33478  rloccring  33504  rlocf1  33507  ricdomn1  33522  dvdsruasso  33614  nsgqusf1olem3  33640  rhmquskerlem  33649  elrspunidl  33652  rhmimaidl  33656  mxidlprm  33670  mxidlirredi  33671  ssmxidl  33674  qsdrngi  33694  qsdrng  33696  1arithidom  33744  1arithufdlem3  33753  r1plmhm  33816  r1pquslmic  33817  mplidomlem  33834  vieta  33887  lbsdiflsp0  33933  fldext2chn  34035  constrconj  34052  constrfin  34053  constrelextdg2  34054  constrfiss  34058  cos9thpiminplylem2  34090  qtophaus  34143  locfinreflem  34147  cmpcref  34157  pstmxmet  34204  lmxrge0  34259  esumcst  34370  omssubadd  34607  signstfvneq0  34876  afsval  34978  matunitlindflem1  38127  heicant  38166  sstotbnd2  38285  primrootscoprmpow  42728  primrootspoweq0  42735  aks6d1c2p2  42748  aks6d1c2lem4  42756  aks6d1c2  42759  unitscyglem3  42826  dffltz  43228  flt4lem7  43253  eldioph2b  43356  diophren  43402  pell1234qrdich  43450  omabs2  43921  iunconnlem2  45508  limcrecl  46203  limclner  46223  icccncfext  46459  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  stoweidlem60  46632  fourierdlem51  46729  fourierdlem77  46755  fourierdlem103  46781  fourierdlem104  46782  smfaddlem1  47335  smfmullem3  47365  chnerlem1  47456  grtriprop  48561  upfval  49805  fuco21  49965