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 735	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  17609  catass  17610  monpropd  17662  subccocl  17770  funcco  17796  funcpropd  17827  mhmmnd  18961  ghmqusnsg  19179  ghmquskerlem3  19183  omndmul2  20030  rhmqusnsg  21210  pm2mpmhmlem2  22722  neitr  23083  restutopopn  24142  ustuqtop4  24148  utopreg  24156  cfilucfil  24463  psmetutop  24471  dyadmax  25515  2sqmo  27364  tgifscgr  28471  tgcgrxfr  28481  tgbtwnconn1lem3  28537  tgbtwnconn1  28538  legov  28548  legtrd  28552  legso  28562  miriso  28633  perpneq  28677  footexALT  28681  footex  28684  colperpex  28696  opphllem  28698  midex  28700  opphl  28717  lnopp2hpgb  28726  trgcopyeu  28769  dfcgra2  28793  inaghl  28808  f1otrg  28834  2ndresdju  32606  nn0xmulclb  32727  chnub  32967  psgnfzto1stlem  33055  cyc3genpm  33107  elrgspnlem4  33195  rloccring  33220  rlocf1  33223  dvdsruasso  33332  nsgqusf1olem3  33362  rhmquskerlem  33372  elrspunidl  33375  rhmimaidl  33379  rhmpreimaprmidl  33398  ssdifidllem  33403  ssdifidlprm  33405  mxidlprm  33417  mxidlirredi  33418  ssmxidl  33421  qsdrngi  33442  qsdrng  33444  1arithidom  33484  1arithufdlem3  33493  r1plmhm  33551  r1pquslmic  33552  lbsdiflsp0  33598  fldext2chn  33694  constrconj  33711  constrfin  33712  constrelextdg2  33713  constrfiss  33717  cos9thpiminplylem2  33749  qtophaus  33802  locfinreflem  33806  cmpcref  33816  pstmxmet  33863  lmxrge0  33918  esumcst  34029  omssubadd  34267  signstfvneq0  34539  afsval  34638  matunitlindflem1  37595  heicant  37634  sstotbnd2  37753  primrootscoprmpow  42072  primrootspoweq0  42079  aks6d1c2p2  42092  aks6d1c2lem4  42100  aks6d1c2  42103  unitscyglem3  42170  dffltz  42607  flt4lem7  42632  eldioph2b  42736  diophren  42786  pell1234qrdich  42834  omabs2  43305  iunconnlem2  44908  limcrecl  45611  limclner  45633  icccncfext  45869  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  stoweidlem60  46042  fourierdlem51  46139  fourierdlem77  46165  fourierdlem103  46191  fourierdlem104  46192  smfaddlem1  46745  smfmullem3  46775  grtriprop  47926  upfval  49162  fuco21  49322