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  18974  neiptopnei  23045  neitx  23520  ustex3sym  24131  restutop  24150  ustuqtop4  24157  utopreg  24165  xrge0tsms  24748  noetainflem4  27677  f1otrg  28847  nn0xmulclb  32749  xrge0tsmsd  33037  elrgspnlem4  33207  imaslmod  33313  elrspunidl  33388  rhmpreimaprmidl  33411  qsidomlem1  33412  mxidlprm  33430  1arithidom  33497  dfufd2  33510  extdg1id  33674  pstmxmet  33905  esumfsup  34078  esum2dlem  34100  esum2d  34101  omssubadd  34308  eulerpartlemgvv  34384  signstfvneq0  34580  satffunlem2lem1  35436  matunitlindflem2  37656  aks6d1c2p2  42151  dffltz  42666  eldioph2  42794  limcrecl  45668  icccncfext  45924  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  stoweidlem60  46097  fourierdlem77  46220  fourierdlem80  46223  fourierdlem103  46246  fourierdlem104  46247  etransclem35  46306