Theorem simp-5l 790

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mhmmnd  19038  neiptopnei  23122  neitx  23597  ustex3sym  24208  restutop  24227  ustuqtop4  24234  utopreg  24242  xrge0tsms  24825  noetainflem4  27729  f1otrg  28964  nn0xmulclb  32870  xrge0tsmsd  33161  elrgspnlem4  33333  imaslmod  33443  elrspunidl  33518  rhmpreimaprmidl  33541  qsidomlem1  33542  mxidlprm  33560  1arithidom  33627  dfufd2  33640  extdg1id  33857  pstmxmet  34088  esumfsup  34261  esum2dlem  34283  esum2d  34284  omssubadd  34491  eulerpartlemgvv  34567  signstfvneq0  34763  satffunlem2lem1  35639  matunitlindflem2  37991  aks6d1c2p2  42611  dffltz  43091  eldioph2  43218  limcrecl  46081  icccncfext  46337  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  stoweidlem60  46510  fourierdlem77  46633  fourierdlem80  46636  fourierdlem103  46659  fourierdlem104  46660  etransclem35  46719