Theorem simp-5l 794

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mhmmnd  19089  neiptopnei  23172  neitx  23647  ustex3sym  24258  restutop  24277  ustuqtop4  24284  utopreg  24292  xrge0tsms  24875  noetainflem4  27781  f1otrg  29017  nn0xmulclb  32923  xrge0tsmsd  33214  elrgspnlem4  33387  rlocisunit  33418  imaslmod  33500  elrspunidl  33575  rhmpreimaprmidl  33599  qsidomlem1  33600  mxidlprm  33619  1arithidom  33694  dfufd2  33707  extdg1id  33924  pstmxmet  34155  esumfsup  34328  esum2dlem  34350  esum2d  34351  omssubadd  34558  eulerpartlemgvv  34634  signstfvneq0  34830  satffunlem2lem1  35718  matunitlindflem2  38080  aks6d1c2p2  42700  dffltz  43180  eldioph2  43307  limcrecl  46169  icccncfext  46425  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  stoweidlem60  46598  fourierdlem77  46721  fourierdlem80  46724  fourierdlem103  46747  fourierdlem104  46748  etransclem35  46807