Theorem simp-5l 796

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 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad5antr 746	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mhmmnd  19131  rhmpreimaprmidl  21460  qsidomlem1  21461  neiptopnei  23270  neitx  23745  ustex3sym  24356  restutop  24375  ustuqtop4  24382  utopreg  24390  xrge0tsms  24973  noetainflem4  27882  f1otrg  29198  nn0xmulclb  33094  xrge0tsmsd  33371  elrgspnlem4  33543  rlocisunit  33574  imaslmod  33651  elrspunidl  33714  mxidlprm  33731  1arithidom  33805  dfufd2  33818  extdg1id  34034  pstmxmet  34265  esumfsup  34438  esum2dlem  34460  esum2d  34461  omssubadd  34668  eulerpartlemgvv  34744  signstfvneq0  34937  satffunlem2lem1  35874  matunitlindflem2  38246  aks6d1c2p2  42864  dffltz  43346  eldioph2  43473  limcrecl  46325  icccncfext  46581  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  stoweidlem60  46754  fourierdlem77  46877  fourierdlem80  46880  fourierdlem103  46903  fourierdlem104  46904  etransclem35  46963