Theorem simp-5l 790

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mhmmnd  19032  neiptopnei  23116  neitx  23591  ustex3sym  24202  restutop  24221  ustuqtop4  24228  utopreg  24236  xrge0tsms  24819  noetainflem4  27723  f1otrg  28958  nn0xmulclb  32864  xrge0tsmsd  33155  elrgspnlem4  33327  imaslmod  33437  elrspunidl  33512  rhmpreimaprmidl  33535  qsidomlem1  33536  mxidlprm  33554  1arithidom  33629  dfufd2  33642  extdg1id  33859  pstmxmet  34090  esumfsup  34263  esum2dlem  34285  esum2d  34286  omssubadd  34493  eulerpartlemgvv  34569  signstfvneq0  34765  satffunlem2lem1  35641  matunitlindflem2  37993  aks6d1c2p2  42613  dffltz  43093  eldioph2  43220  limcrecl  46082  icccncfext  46338  ioodvbdlimc1lem2  46383  ioodvbdlimc2lem  46385  stoweidlem60  46511  fourierdlem77  46634  fourierdlem80  46637  fourierdlem103  46660  fourierdlem104  46661  etransclem35  46720