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 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  19104  neiptopnei  23161  neitx  23636  ustex3sym  24247  restutop  24267  ustuqtop4  24274  utopreg  24282  xrge0tsms  24875  noetainflem4  27803  f1otrg  28897  nn0xmulclb  32778  xrge0tsmsd  33041  imaslmod  33346  elrspunidl  33421  rhmpreimaprmidl  33444  qsidomlem1  33445  mxidlprm  33463  1arithidom  33530  dfufd2  33543  extdg1id  33676  pstmxmet  33843  esumfsup  34034  esum2dlem  34056  esum2d  34057  omssubadd  34265  eulerpartlemgvv  34341  signstfvneq0  34549  satffunlem2lem1  35372  matunitlindflem2  37577  aks6d1c2p2  42076  dffltz  42589  eldioph2  42718  limcrecl  45550  icccncfext  45808  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweidlem60  45981  fourierdlem77  46104  fourierdlem80  46107  fourierdlem103  46130  fourierdlem104  46131  etransclem35  46190