Theorem simp-5l 783

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 732	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 206  df-an 397

This theorem is referenced by:  mhmmnd  18949  neiptopnei  22643  neitx  23118  ustex3sym  23729  restutop  23749  ustuqtop4  23756  utopreg  23764  xrge0tsms  24357  noetainflem4  27250  f1otrg  28160  nn0xmulclb  32022  xrge0tsmsd  32250  imaslmod  32509  elrspunidl  32591  rhmpreimaprmidl  32615  qsidomlem1  32616  mxidlprm  32631  extdg1id  32801  pstmxmet  32946  esumfsup  33137  esum2dlem  33159  esum2d  33160  omssubadd  33368  eulerpartlemgvv  33444  signstfvneq0  33652  satffunlem2lem1  34464  matunitlindflem2  36571  aks6d1c2p2  41043  dffltz  41458  eldioph2  41582  limcrecl  44424  icccncfext  44682  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  stoweidlem60  44855  fourierdlem77  44978  fourierdlem80  44981  fourierdlem103  45004  fourierdlem104  45005  etransclem35  45064