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 734	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  18996  neiptopnei  23019  neitx  23494  ustex3sym  24105  restutop  24125  ustuqtop4  24132  utopreg  24140  xrge0tsms  24723  noetainflem4  27652  f1otrg  28798  nn0xmulclb  32694  xrge0tsmsd  33002  elrgspnlem4  33196  imaslmod  33324  elrspunidl  33399  rhmpreimaprmidl  33422  qsidomlem1  33423  mxidlprm  33441  1arithidom  33508  dfufd2  33521  extdg1id  33661  pstmxmet  33887  esumfsup  34060  esum2dlem  34082  esum2d  34083  omssubadd  34291  eulerpartlemgvv  34367  signstfvneq0  34563  satffunlem2lem1  35391  matunitlindflem2  37611  aks6d1c2p2  42107  dffltz  42622  eldioph2  42750  limcrecl  45627  icccncfext  45885  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem60  46058  fourierdlem77  46181  fourierdlem80  46184  fourierdlem103  46207  fourierdlem104  46208  etransclem35  46267