Theorem simp-5r 782

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 731	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 206  df-an 396

This theorem is referenced by:  catcocl  17311  catass  17312  monpropd  17366  subccocl  17476  funcco  17502  funcpropd  17532  mhmmnd  18612  pm2mpmhmlem2  21876  neitr  22239  restutopopn  23298  ustuqtop4  23304  utopreg  23312  cfilucfil  23621  psmetutop  23629  dyadmax  24667  2sqmo  26490  tgifscgr  26773  tgcgrxfr  26783  tgbtwnconn1lem3  26839  tgbtwnconn1  26840  legov  26850  legtrd  26854  legso  26864  miriso  26935  perpneq  26979  footexALT  26983  footex  26986  colperpex  26998  opphllem  27000  midex  27002  opphl  27019  lnopp2hpgb  27028  trgcopyeu  27071  dfcgra2  27095  inaghl  27110  f1otrg  27136  2ndresdju  30887  nn0xmulclb  30996  omndmul2  31240  psgnfzto1stlem  31269  cyc3genpm  31321  nsgqusf1olem3  31502  elrspunidl  31508  rhmimaidl  31511  rhmpreimaprmidl  31529  mxidlprm  31542  ssmxidl  31544  lbsdiflsp0  31609  qtophaus  31688  locfinreflem  31692  cmpcref  31702  pstmxmet  31749  lmxrge0  31804  esumcst  31931  omssubadd  32167  signstfvneq0  32451  afsval  32551  matunitlindflem1  35700  heicant  35739  sstotbnd2  35859  dffltz  40387  flt4lem7  40412  eldioph2b  40501  diophren  40551  pell1234qrdich  40599  iunconnlem2  42444  limcrecl  43060  limclner  43082  icccncfext  43318  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem60  43491  fourierdlem51  43588  fourierdlem77  43614  fourierdlem103  43640  fourierdlem104  43641  smfaddlem1  44185  smfmullem3  44214