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 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  19095  neiptopnei  23156  neitx  23631  ustex3sym  24242  restutop  24262  ustuqtop4  24269  utopreg  24277  xrge0tsms  24870  noetainflem4  27800  f1otrg  28894  nn0xmulclb  32782  xrge0tsmsd  33048  elrgspnlem4  33235  imaslmod  33361  elrspunidl  33436  rhmpreimaprmidl  33459  qsidomlem1  33460  mxidlprm  33478  1arithidom  33545  dfufd2  33558  extdg1id  33691  pstmxmet  33858  esumfsup  34051  esum2dlem  34073  esum2d  34074  omssubadd  34282  eulerpartlemgvv  34358  signstfvneq0  34566  satffunlem2lem1  35389  matunitlindflem2  37604  aks6d1c2p2  42101  dffltz  42621  eldioph2  42750  limcrecl  45585  icccncfext  45843  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  stoweidlem60  46016  fourierdlem77  46139  fourierdlem80  46142  fourierdlem103  46165  fourierdlem104  46166  etransclem35  46225