Theorem simp-5l 781

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 730	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 206  df-an 396

This theorem is referenced by:  mhmmnd  18612  neiptopnei  22191  neitx  22666  ustex3sym  23277  restutop  23297  ustuqtop4  23304  utopreg  23312  xrge0tsms  23903  f1otrg  27136  nn0xmulclb  30996  xrge0tsmsd  31219  imaslmod  31455  elrspunidl  31508  rhmpreimaprmidl  31529  qsidomlem1  31530  mxidlprm  31542  extdg1id  31640  pstmxmet  31749  esumfsup  31938  esum2dlem  31960  esum2d  31961  omssubadd  32167  eulerpartlemgvv  32243  signstfvneq0  32451  satffunlem2lem1  33266  noetainflem4  33870  matunitlindflem2  35701  dffltz  40387  eldioph2  40500  limcrecl  43060  icccncfext  43318  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem60  43491  fourierdlem77  43614  fourierdlem80  43617  fourierdlem103  43640  fourierdlem104  43641  etransclem35  43700