Theorem simp-5l 783

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mhmmnd  18221  neiptopnei  21740  neitx  22215  ustex3sym  22826  restutop  22846  ustuqtop4  22853  utopreg  22861  xrge0tsms  23442  f1otrg  26657  nn0xmulclb  30496  xrge0tsmsd  30692  imaslmod  30922  qsidomlem1  30965  mxidlprm  30977  extdg1id  31053  pstmxmet  31137  esumfsup  31329  esum2dlem  31351  esum2d  31352  omssubadd  31558  eulerpartlemgvv  31634  signstfvneq0  31842  satffunlem2lem1  32651  matunitlindflem2  34904  dffltz  39291  eldioph2  39379  limcrecl  41930  icccncfext  42190  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  stoweidlem60  42365  fourierdlem77  42488  fourierdlem80  42491  fourierdlem103  42514  fourierdlem104  42515  etransclem35  42574