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 735	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  19031  neiptopnei  23107  neitx  23582  ustex3sym  24193  restutop  24212  ustuqtop4  24219  utopreg  24227  xrge0tsms  24810  noetainflem4  27718  f1otrg  28953  nn0xmulclb  32859  xrge0tsmsd  33149  elrgspnlem4  33321  imaslmod  33428  elrspunidl  33503  rhmpreimaprmidl  33526  qsidomlem1  33527  mxidlprm  33545  1arithidom  33612  dfufd2  33625  extdg1id  33826  pstmxmet  34057  esumfsup  34230  esum2dlem  34252  esum2d  34253  omssubadd  34460  eulerpartlemgvv  34536  signstfvneq0  34732  satffunlem2lem1  35602  matunitlindflem2  37952  aks6d1c2p2  42572  dffltz  43081  eldioph2  43208  limcrecl  46077  icccncfext  46333  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  stoweidlem60  46506  fourierdlem77  46629  fourierdlem80  46632  fourierdlem103  46655  fourierdlem104  46656  etransclem35  46715