Theorem simp-5r 786

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 736	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  17642  catass  17643  monpropd  17695  subccocl  17803  funcco  17829  funcpropd  17860  chnub  18579  mhmmnd  19031  ghmqusnsg  19248  ghmquskerlem3  19252  omndmul2  20099  rhmqusnsg  21275  pm2mpmhmlem2  22794  neitr  23155  restutopopn  24213  ustuqtop4  24219  utopreg  24227  cfilucfil  24534  psmetutop  24542  dyadmax  25575  2sqmo  27414  tgifscgr  28590  tgcgrxfr  28600  tgbtwnconn1lem3  28656  tgbtwnconn1  28657  legov  28667  legtrd  28671  legso  28681  miriso  28752  perpneq  28796  footexALT  28800  footex  28803  colperpex  28815  opphllem  28817  midex  28819  opphl  28836  lnopp2hpgb  28845  trgcopyeu  28888  dfcgra2  28912  inaghl  28927  f1otrg  28953  2ndresdju  32737  nn0xmulclb  32859  psgnfzto1stlem  33176  cyc3genpm  33228  elrgspnlem4  33321  rloccring  33346  rlocf1  33349  dvdsruasso  33460  nsgqusf1olem3  33490  rhmquskerlem  33500  elrspunidl  33503  rhmimaidl  33507  rhmpreimaprmidl  33526  ssdifidllem  33531  ssdifidlprm  33533  mxidlprm  33545  mxidlirredi  33546  ssmxidl  33549  qsdrngi  33570  qsdrng  33572  1arithidom  33612  1arithufdlem3  33621  r1plmhm  33685  r1pquslmic  33686  vieta  33739  lbsdiflsp0  33786  fldext2chn  33888  constrconj  33905  constrfin  33906  constrelextdg2  33907  constrfiss  33911  cos9thpiminplylem2  33943  qtophaus  33996  locfinreflem  34000  cmpcref  34010  pstmxmet  34057  lmxrge0  34112  esumcst  34223  omssubadd  34460  signstfvneq0  34732  afsval  34831  matunitlindflem1  37951  heicant  37990  sstotbnd2  38109  primrootscoprmpow  42552  primrootspoweq0  42559  aks6d1c2p2  42572  aks6d1c2lem4  42580  aks6d1c2  42583  unitscyglem3  42650  dffltz  43081  flt4lem7  43106  eldioph2b  43209  diophren  43259  pell1234qrdich  43307  omabs2  43778  iunconnlem2  45379  limcrecl  46077  limclner  46097  icccncfext  46333  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  stoweidlem60  46506  fourierdlem51  46603  fourierdlem77  46629  fourierdlem103  46655  fourierdlem104  46656  smfaddlem1  47209  smfmullem3  47239  chnerlem1  47328  grtriprop  48429  upfval  49663  fuco21  49823