Theorem simp-5l 764

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

Syntax hints:   → wi 4   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  simp-6lOLD  769  mhmmnd  17744  neiptopnei  21156  neitx  21630  ustex3sym  22240  restutop  22260  ustuqtop4  22267  utopreg  22275  xrge0tsms  22856  f1otrg  25971  xrge0tsmsd  30119  pstmxmet  30274  esumfsup  30466  esum2dlem  30488  esum2d  30489  omssubadd  30696  eulerpartlemgvv  30772  matunitlindflem2  33732  eldioph2  37844  limcrecl  40373  icccncfext  40612  ioodvbdlimc1lem2  40659  ioodvbdlimc2lem  40661  stoweidlem60  40788  fourierdlem77  40911  fourierdlem80  40914  fourierdlem103  40937  fourierdlem104  40938  etransclem35  40997