Theorem simp-5r 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-5r	⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simp-5r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad5antlr 732	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  catcocl  17394  catass  17395  monpropd  17449  subccocl  17560  funcco  17586  funcpropd  17616  mhmmnd  18697  pm2mpmhmlem2  21968  neitr  22331  restutopopn  23390  ustuqtop4  23396  utopreg  23404  cfilucfil  23715  psmetutop  23723  dyadmax  24762  2sqmo  26585  tgifscgr  26869  tgcgrxfr  26879  tgbtwnconn1lem3  26935  tgbtwnconn1  26936  legov  26946  legtrd  26950  legso  26960  miriso  27031  perpneq  27075  footexALT  27079  footex  27082  colperpex  27094  opphllem  27096  midex  27098  opphl  27115  lnopp2hpgb  27124  trgcopyeu  27167  dfcgra2  27191  inaghl  27206  f1otrg  27232  2ndresdju  30986  nn0xmulclb  31094  omndmul2  31338  psgnfzto1stlem  31367  cyc3genpm  31419  nsgqusf1olem3  31600  elrspunidl  31606  rhmimaidl  31609  rhmpreimaprmidl  31627  mxidlprm  31640  ssmxidl  31642  lbsdiflsp0  31707  qtophaus  31786  locfinreflem  31790  cmpcref  31800  pstmxmet  31847  lmxrge0  31902  esumcst  32031  omssubadd  32267  signstfvneq0  32551  afsval  32651  matunitlindflem1  35773  heicant  35812  sstotbnd2  35932  dffltz  40471  flt4lem7  40496  eldioph2b  40585  diophren  40635  pell1234qrdich  40683  iunconnlem2  42555  limcrecl  43170  limclner  43192  icccncfext  43428  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  stoweidlem60  43601  fourierdlem51  43698  fourierdlem77  43724  fourierdlem103  43750  fourierdlem104  43751  smfaddlem1  44298  smfmullem3  44327