Theorem simp-5l 796

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mhmmnd  19121  rhmpreimaprmidl  21439  qsidomlem1  21440  neiptopnei  23250  neitx  23725  ustex3sym  24336  restutop  24355  ustuqtop4  24362  utopreg  24370  xrge0tsms  24953  noetainflem4  27862  f1otrg  29129  nn0xmulclb  33028  xrge0tsmsd  33306  elrgspnlem4  33478  rlocisunit  33509  imaslmod  33588  elrspunidl  33652  mxidlprm  33670  1arithidom  33744  dfufd2  33757  extdg1id  33973  pstmxmet  34204  esumfsup  34377  esum2dlem  34399  esum2d  34400  omssubadd  34607  eulerpartlemgvv  34683  signstfvneq0  34876  satffunlem2lem1  35767  matunitlindflem2  38128  aks6d1c2p2  42748  dffltz  43228  eldioph2  43355  limcrecl  46203  icccncfext  46459  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  stoweidlem60  46632  fourierdlem77  46755  fourierdlem80  46758  fourierdlem103  46781  fourierdlem104  46782  etransclem35  46841