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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  mhmmnd  18947  neiptopnei  22636  neitx  23111  ustex3sym  23722  restutop  23742  ustuqtop4  23749  utopreg  23757  xrge0tsms  24350  noetainflem4  27243  f1otrg  28122  nn0xmulclb  31984  xrge0tsmsd  32209  imaslmod  32468  elrspunidl  32546  rhmpreimaprmidl  32570  qsidomlem1  32571  mxidlprm  32586  extdg1id  32742  pstmxmet  32877  esumfsup  33068  esum2dlem  33090  esum2d  33091  omssubadd  33299  eulerpartlemgvv  33375  signstfvneq0  33583  satffunlem2lem1  34395  matunitlindflem2  36485  aks6d1c2p2  40957  dffltz  41376  eldioph2  41500  limcrecl  44345  icccncfext  44603  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  stoweidlem60  44776  fourierdlem77  44899  fourierdlem80  44902  fourierdlem103  44925  fourierdlem104  44926  etransclem35  44985