Theorem simp-5r 784

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  catcocl  16956  catass  16957  monpropd  17007  subccocl  17115  funcco  17141  funcpropd  17170  mhmmnd  18221  pm2mpmhmlem2  21427  neitr  21788  restutopopn  22847  ustuqtop4  22853  utopreg  22861  cfilucfil  23169  psmetutop  23177  dyadmax  24199  2sqmo  26013  tgifscgr  26294  tgcgrxfr  26304  tgbtwnconn1lem3  26360  tgbtwnconn1  26361  legov  26371  legtrd  26375  legso  26385  miriso  26456  perpneq  26500  footexALT  26504  footex  26507  colperpex  26519  opphllem  26521  midex  26523  opphl  26540  lnopp2hpgb  26549  trgcopyeu  26592  dfcgra2  26616  inaghl  26631  f1otrg  26657  nn0xmulclb  30496  omndmul2  30713  psgnfzto1stlem  30742  cyc3genpm  30794  mxidlprm  30977  ssmxidl  30979  lbsdiflsp0  31022  qtophaus  31100  locfinreflem  31104  cmpcref  31114  pstmxmet  31137  lmxrge0  31195  esumcst  31322  omssubadd  31558  signstfvneq0  31842  afsval  31942  matunitlindflem1  34903  heicant  34942  sstotbnd2  35067  dffltz  39291  eldioph2b  39380  diophren  39430  pell1234qrdich  39478  iunconnlem2  41289  limcrecl  41930  limclner  41952  icccncfext  42190  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  stoweidlem60  42365  fourierdlem51  42462  fourierdlem77  42488  fourierdlem103  42514  fourierdlem104  42515  smfaddlem1  43059  smfmullem3  43088