Theorem simp-5r 784

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  catcocl  17698  catass  17699  monpropd  17753  subccocl  17864  funcco  17890  funcpropd  17922  mhmmnd  19058  ghmqusnsg  19276  ghmquskerlem3  19280  rhmqusnsg  21274  pm2mpmhmlem2  22812  neitr  23175  restutopopn  24234  ustuqtop4  24240  utopreg  24248  cfilucfil  24559  psmetutop  24567  dyadmax  25618  2sqmo  27466  tgifscgr  28435  tgcgrxfr  28445  tgbtwnconn1lem3  28501  tgbtwnconn1  28502  legov  28512  legtrd  28516  legso  28526  miriso  28597  perpneq  28641  footexALT  28645  footex  28648  colperpex  28660  opphllem  28662  midex  28664  opphl  28681  lnopp2hpgb  28690  trgcopyeu  28733  dfcgra2  28757  inaghl  28772  f1otrg  28798  2ndresdju  32566  nn0xmulclb  32675  chnub  32881  omndmul2  32947  psgnfzto1stlem  32978  cyc3genpm  33030  rloccring  33125  rlocf1  33128  dvdsruasso  33260  nsgqusf1olem3  33290  rhmquskerlem  33300  elrspunidl  33303  rhmimaidl  33307  rhmpreimaprmidl  33326  ssdifidllem  33331  ssdifidlprm  33333  mxidlprm  33345  mxidlirredi  33346  ssmxidl  33349  qsdrngi  33370  qsdrng  33372  1arithidom  33412  1arithufdlem3  33421  r1plmhm  33477  r1pquslmic  33478  lbsdiflsp0  33521  constrconj  33603  fldext2chn  33606  qtophaus  33651  locfinreflem  33655  cmpcref  33665  pstmxmet  33712  lmxrge0  33767  esumcst  33896  omssubadd  34134  signstfvneq0  34418  afsval  34517  matunitlindflem1  37317  heicant  37356  sstotbnd2  37475  primrootscoprmpow  41797  primrootspoweq0  41804  aks6d1c2p2  41817  aks6d1c2lem4  41825  aks6d1c2  41828  dffltz  42288  flt4lem7  42313  eldioph2b  42420  diophren  42470  pell1234qrdich  42518  omabs2  42998  iunconnlem2  44611  limcrecl  45250  limclner  45272  icccncfext  45508  ioodvbdlimc1lem2  45553  ioodvbdlimc2lem  45555  stoweidlem60  45681  fourierdlem51  45778  fourierdlem77  45804  fourierdlem103  45830  fourierdlem104  45831  smfaddlem1  46384  smfmullem3  46414