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  19052  neiptopnei  23075  neitx  23550  ustex3sym  24161  restutop  24181  ustuqtop4  24188  utopreg  24196  xrge0tsms  24779  noetainflem4  27709  f1otrg  28855  nn0xmulclb  32753  xrge0tsmsd  33061  elrgspnlem4  33245  imaslmod  33373  elrspunidl  33448  rhmpreimaprmidl  33471  qsidomlem1  33472  mxidlprm  33490  1arithidom  33557  dfufd2  33570  extdg1id  33712  pstmxmet  33933  esumfsup  34106  esum2dlem  34128  esum2d  34129  omssubadd  34337  eulerpartlemgvv  34413  signstfvneq0  34609  satffunlem2lem1  35431  matunitlindflem2  37646  aks6d1c2p2  42137  dffltz  42624  eldioph2  42752  limcrecl  45625  icccncfext  45883  ioodvbdlimc1lem2  45928  ioodvbdlimc2lem  45930  stoweidlem60  46056  fourierdlem77  46179  fourierdlem80  46182  fourierdlem103  46205  fourierdlem104  46206  etransclem35  46265