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  18994  neiptopnei  23076  neitx  23551  ustex3sym  24162  restutop  24181  ustuqtop4  24188  utopreg  24196  xrge0tsms  24779  noetainflem4  27708  f1otrg  28943  nn0xmulclb  32851  xrge0tsmsd  33155  elrgspnlem4  33327  imaslmod  33434  elrspunidl  33509  rhmpreimaprmidl  33532  qsidomlem1  33533  mxidlprm  33551  1arithidom  33618  dfufd2  33631  extdg1id  33823  pstmxmet  34054  esumfsup  34227  esum2dlem  34249  esum2d  34250  omssubadd  34457  eulerpartlemgvv  34533  signstfvneq0  34729  satffunlem2lem1  35598  matunitlindflem2  37814  aks6d1c2p2  42369  dffltz  42873  eldioph2  43000  limcrecl  45871  icccncfext  46127  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  stoweidlem60  46300  fourierdlem77  46423  fourierdlem80  46426  fourierdlem103  46449  fourierdlem104  46450  etransclem35  46509