Theorem simp-5l 785

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mhmmnd  19006  neiptopnei  23088  neitx  23563  ustex3sym  24174  restutop  24193  ustuqtop4  24200  utopreg  24208  xrge0tsms  24791  noetainflem4  27720  f1otrg  28955  nn0xmulclb  32861  xrge0tsmsd  33166  elrgspnlem4  33338  imaslmod  33445  elrspunidl  33520  rhmpreimaprmidl  33543  qsidomlem1  33544  mxidlprm  33562  1arithidom  33629  dfufd2  33642  extdg1id  33843  pstmxmet  34074  esumfsup  34247  esum2dlem  34269  esum2d  34270  omssubadd  34477  eulerpartlemgvv  34553  signstfvneq0  34749  satffunlem2lem1  35617  matunitlindflem2  37862  aks6d1c2p2  42483  dffltz  42986  eldioph2  43113  limcrecl  45983  icccncfext  46239  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  stoweidlem60  46412  fourierdlem77  46535  fourierdlem80  46538  fourierdlem103  46561  fourierdlem104  46562  etransclem35  46621