Theorem simp-5l 797

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-5l	⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)

Proof of Theorem simp-5l

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad5antr 747	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mhmmnd  19254  rhmpreimaprmidl  21615  qsidomlem1  21616  matunitlindflem2  22975  neiptopnei  23430  neitx  23906  ustex3sym  24517  restutop  24536  ustuqtop4  24543  utopreg  24551  xrge0tsms  25134  noetainflem4  28079  f1otrg  29430  nn0xmulclb  33345  xrge0tsmsd  33616  elrgspnlem4  33788  rlocisunit  33819  imaslmod  33896  elrspunidl  33960  mxidlprm  33977  1arithidom  34051  dfufd2  34064  extdg1id  34280  pstmxmet  34511  esumfsup  34684  esum2dlem  34706  esum2d  34707  omssubadd  34915  eulerpartlemgvv  34991  signstfvneq0  35184  satffunlem2lem1  36138  mh-inf3f1  37299  aks6d1c2p2  43137  dffltz  43624  eldioph2  43726  limcrecl  46585  icccncfext  46841  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  stoweidlem60  47014  fourierdlem77  47137  fourierdlem80  47140  fourierdlem103  47163  fourierdlem104  47164  etransclem35  47223