Theorem simp-5r 785

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 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad5antlr 734	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:  catcocl  17743  catass  17744  monpropd  17798  subccocl  17909  funcco  17935  funcpropd  17967  mhmmnd  19104  ghmqusnsg  19322  ghmquskerlem3  19326  rhmqusnsg  21318  pm2mpmhmlem2  22846  neitr  23209  restutopopn  24268  ustuqtop4  24274  utopreg  24282  cfilucfil  24593  psmetutop  24601  dyadmax  25652  2sqmo  27499  tgifscgr  28534  tgcgrxfr  28544  tgbtwnconn1lem3  28600  tgbtwnconn1  28601  legov  28611  legtrd  28615  legso  28625  miriso  28696  perpneq  28740  footexALT  28744  footex  28747  colperpex  28759  opphllem  28761  midex  28763  opphl  28780  lnopp2hpgb  28789  trgcopyeu  28832  dfcgra2  28856  inaghl  28871  f1otrg  28897  2ndresdju  32667  nn0xmulclb  32778  chnub  32984  omndmul2  33062  psgnfzto1stlem  33093  cyc3genpm  33145  rloccring  33242  rlocf1  33245  dvdsruasso  33378  nsgqusf1olem3  33408  rhmquskerlem  33418  elrspunidl  33421  rhmimaidl  33425  rhmpreimaprmidl  33444  ssdifidllem  33449  ssdifidlprm  33451  mxidlprm  33463  mxidlirredi  33464  ssmxidl  33467  qsdrngi  33488  qsdrng  33490  1arithidom  33530  1arithufdlem3  33539  r1plmhm  33595  r1pquslmic  33596  lbsdiflsp0  33639  fldext2chn  33719  constrconj  33735  constrfin  33736  constrelextdg2  33737  qtophaus  33782  locfinreflem  33786  cmpcref  33796  pstmxmet  33843  lmxrge0  33898  esumcst  34027  omssubadd  34265  signstfvneq0  34549  afsval  34648  matunitlindflem1  37576  heicant  37615  sstotbnd2  37734  primrootscoprmpow  42056  primrootspoweq0  42063  aks6d1c2p2  42076  aks6d1c2lem4  42084  aks6d1c2  42087  unitscyglem3  42154  dffltz  42589  flt4lem7  42614  eldioph2b  42719  diophren  42769  pell1234qrdich  42817  omabs2  43294  iunconnlem2  44906  limcrecl  45550  limclner  45572  icccncfext  45808  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweidlem60  45981  fourierdlem51  46078  fourierdlem77  46104  fourierdlem103  46130  fourierdlem104  46131  smfaddlem1  46684  smfmullem3  46714  grtriprop  47792