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  19279  rhmpreimaprmidl  21640  qsidomlem1  21641  matunitlindflem2  23000  neiptopnei  23455  neitx  23931  ustex3sym  24542  restutop  24561  ustuqtop4  24568  utopreg  24576  xrge0tsms  25159  noetainflem4  28102  f1otrg  29453  nn0xmulclb  33409  xrge0tsmsd  33680  elrgspnlem4  33852  rlocisunit  33883  imaslmod  33960  elrspunidl  34024  mxidlprm  34041  1arithidom  34115  dfufd2  34128  extdg1id  34344  pstmxmet  34575  esumfsup  34748  esum2dlem  34770  esum2d  34771  omssubadd  34978  eulerpartlemgvv  35054  signstfvneq0  35247  satffunlem2lem1  36255  mh-inf3f1  37421  aks6d1c2p2  43262  dffltz  43763  eldioph2  43866  limcrecl  46734  icccncfext  46990  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  stoweidlem60  47163  fourierdlem77  47286  fourierdlem80  47289  fourierdlem103  47312  fourierdlem104  47313  etransclem35  47372