Theorem simp-5l 797

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 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad5antr 747	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mhmmnd  19193  rhmpreimaprmidl  21548  qsidomlem1  21549  matunitlindflem2  22908  neiptopnei  23363  neitx  23839  ustex3sym  24450  restutop  24469  ustuqtop4  24476  utopreg  24484  xrge0tsms  25067  noetainflem4  27984  f1otrg  29335  nn0xmulclb  33250  xrge0tsmsd  33521  elrgspnlem4  33693  rlocisunit  33724  imaslmod  33801  elrspunidl  33864  mxidlprm  33881  1arithidom  33955  dfufd2  33968  extdg1id  34184  pstmxmet  34415  esumfsup  34588  esum2dlem  34610  esum2d  34611  omssubadd  34819  eulerpartlemgvv  34895  signstfvneq0  35088  satffunlem2lem1  35991  aks6d1c2p2  42993  dffltz  43488  eldioph2  43615  limcrecl  46467  icccncfext  46723  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  stoweidlem60  46896  fourierdlem77  47019  fourierdlem80  47022  fourierdlem103  47045  fourierdlem104  47046  etransclem35  47105