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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  catcocl  16948  catass  16949  monpropd  16999  subccocl  17107  funcco  17133  funcpropd  17162  mhmmnd  18213  pm2mpmhmlem2  21424  neitr  21785  restutopopn  22844  ustuqtop4  22850  utopreg  22858  cfilucfil  23166  psmetutop  23174  dyadmax  24202  2sqmo  26021  tgifscgr  26302  tgcgrxfr  26312  tgbtwnconn1lem3  26368  tgbtwnconn1  26369  legov  26379  legtrd  26383  legso  26393  miriso  26464  perpneq  26508  footexALT  26512  footex  26515  colperpex  26527  opphllem  26529  midex  26531  opphl  26548  lnopp2hpgb  26557  trgcopyeu  26600  dfcgra2  26624  inaghl  26639  f1otrg  26665  2ndresdju  30411  nn0xmulclb  30522  omndmul2  30763  psgnfzto1stlem  30792  cyc3genpm  30844  elrspunidl  31014  rhmimaidl  31017  rhmpreimaprmidl  31035  mxidlprm  31048  ssmxidl  31050  lbsdiflsp0  31110  qtophaus  31189  locfinreflem  31193  cmpcref  31203  pstmxmet  31250  lmxrge0  31305  esumcst  31432  omssubadd  31668  signstfvneq0  31952  afsval  32052  matunitlindflem1  35053  heicant  35092  sstotbnd2  35212  dffltz  39615  eldioph2b  39704  diophren  39754  pell1234qrdich  39802  iunconnlem2  41641  limcrecl  42271  limclner  42293  icccncfext  42529  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  stoweidlem60  42702  fourierdlem51  42799  fourierdlem77  42825  fourierdlem103  42851  fourierdlem104  42852  smfaddlem1  43396  smfmullem3  43425