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  19161  rhmpreimaprmidl  21516  qsidomlem1  21517  neiptopnei  23326  neitx  23801  ustex3sym  24412  restutop  24431  ustuqtop4  24438  utopreg  24446  xrge0tsms  25029  noetainflem4  27941  f1otrg  29257  nn0xmulclb  33153  xrge0tsmsd  33424  elrgspnlem4  33596  rlocisunit  33627  imaslmod  33704  elrspunidl  33767  mxidlprm  33784  1arithidom  33858  dfufd2  33871  extdg1id  34087  pstmxmet  34318  esumfsup  34491  esum2dlem  34513  esum2d  34514  omssubadd  34722  eulerpartlemgvv  34798  signstfvneq0  34991  satffunlem2lem1  35917  matunitlindflem2  38309  aks6d1c2p2  42927  dffltz  43407  eldioph2  43534  limcrecl  46386  icccncfext  46642  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  stoweidlem60  46815  fourierdlem77  46938  fourierdlem80  46941  fourierdlem103  46964  fourierdlem104  46965  etransclem35  47024