Theorem simp-5l 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-5l	⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)

Proof of Theorem simp-5l

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad5antr 734	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:  mhmmnd  18979  neiptopnei  23048  neitx  23523  ustex3sym  24134  restutop  24153  ustuqtop4  24160  utopreg  24168  xrge0tsms  24751  noetainflem4  27680  f1otrg  28850  nn0xmulclb  32758  xrge0tsmsd  33049  elrgspnlem4  33219  imaslmod  33325  elrspunidl  33400  rhmpreimaprmidl  33423  qsidomlem1  33424  mxidlprm  33442  1arithidom  33509  dfufd2  33522  extdg1id  33700  pstmxmet  33931  esumfsup  34104  esum2dlem  34126  esum2d  34127  omssubadd  34334  eulerpartlemgvv  34410  signstfvneq0  34606  satffunlem2lem1  35469  matunitlindflem2  37677  aks6d1c2p2  42232  dffltz  42752  eldioph2  42879  limcrecl  45753  icccncfext  46009  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  stoweidlem60  46182  fourierdlem77  46305  fourierdlem80  46308  fourierdlem103  46331  fourierdlem104  46332  etransclem35  46391