Theorem simp-5l 784

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 734	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  18961  neiptopnei  23035  neitx  23510  ustex3sym  24121  restutop  24141  ustuqtop4  24148  utopreg  24156  xrge0tsms  24739  noetainflem4  27668  f1otrg  28834  nn0xmulclb  32727  xrge0tsmsd  33028  elrgspnlem4  33195  imaslmod  33300  elrspunidl  33375  rhmpreimaprmidl  33398  qsidomlem1  33399  mxidlprm  33417  1arithidom  33484  dfufd2  33497  extdg1id  33637  pstmxmet  33863  esumfsup  34036  esum2dlem  34058  esum2d  34059  omssubadd  34267  eulerpartlemgvv  34343  signstfvneq0  34539  satffunlem2lem1  35376  matunitlindflem2  37596  aks6d1c2p2  42092  dffltz  42607  eldioph2  42735  limcrecl  45611  icccncfext  45869  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  stoweidlem60  46042  fourierdlem77  46165  fourierdlem80  46168  fourierdlem103  46191  fourierdlem104  46192  etransclem35  46251