Theorem simp-5l 783

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  mhmmnd  19025  neiptopnei  23054  neitx  23529  ustex3sym  24140  restutop  24160  ustuqtop4  24167  utopreg  24175  xrge0tsms  24768  noetainflem4  27691  f1otrg  28693  nn0xmulclb  32559  xrge0tsmsd  32789  imaslmod  33083  elrspunidl  33162  rhmpreimaprmidl  33185  qsidomlem1  33186  mxidlprm  33201  extdg1id  33360  pstmxmet  33503  esumfsup  33694  esum2dlem  33716  esum2d  33717  omssubadd  33925  eulerpartlemgvv  34001  signstfvneq0  34209  satffunlem2lem1  35019  matunitlindflem2  37095  aks6d1c2p2  41594  dffltz  42061  eldioph2  42185  limcrecl  45019  icccncfext  45277  ioodvbdlimc1lem2  45322  ioodvbdlimc2lem  45324  stoweidlem60  45450  fourierdlem77  45573  fourierdlem80  45576  fourierdlem103  45599  fourierdlem104  45600  etransclem35  45659