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  19303  rhmpreimaprmidl  21665  qsidomlem1  21666  matunitlindflem2  23025  neiptopnei  23480  neitx  23956  ustex3sym  24567  restutop  24586  ustuqtop4  24593  utopreg  24601  xrge0tsms  25184  noetainflem4  28127  f1otrg  29478  nn0xmulclb  33433  xrge0tsmsd  33704  elrgspnlem4  33876  rlocisunit  33907  imaslmod  33984  elrspunidl  34048  mxidlprm  34065  1arithidom  34139  dfufd2  34152  extdg1id  34368  pstmxmet  34599  esumfsup  34772  esum2dlem  34794  esum2d  34795  omssubadd  35002  eulerpartlemgvv  35078  signstfvneq0  35271  satffunlem2lem1  36336  mh-inf3f1  37507  aks6d1c2p2  43361  dffltz  43863  eldioph2  43966  limcrecl  46846  icccncfext  47102  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  stoweidlem60  47275  fourierdlem77  47398  fourierdlem80  47401  fourierdlem103  47424  fourierdlem104  47425  etransclem35  47484