Theorem simp-5l 782

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  mhmmnd  18697  neiptopnei  22283  neitx  22758  ustex3sym  23369  restutop  23389  ustuqtop4  23396  utopreg  23404  xrge0tsms  23997  f1otrg  27232  nn0xmulclb  31094  xrge0tsmsd  31317  imaslmod  31553  elrspunidl  31606  rhmpreimaprmidl  31627  qsidomlem1  31628  mxidlprm  31640  extdg1id  31738  pstmxmet  31847  esumfsup  32038  esum2dlem  32060  esum2d  32061  omssubadd  32267  eulerpartlemgvv  32343  signstfvneq0  32551  satffunlem2lem1  33366  noetainflem4  33943  matunitlindflem2  35774  dffltz  40471  eldioph2  40584  limcrecl  43170  icccncfext  43428  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  stoweidlem60  43601  fourierdlem77  43724  fourierdlem80  43727  fourierdlem103  43750  fourierdlem104  43751  etransclem35  43810