Theorem simp-5l 784

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 734	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 207  df-an 396

This theorem is referenced by:  mhmmnd  19034  neiptopnei  23057  neitx  23532  ustex3sym  24143  restutop  24163  ustuqtop4  24170  utopreg  24178  xrge0tsms  24761  noetainflem4  27690  f1otrg  28784  nn0xmulclb  32685  xrge0tsmsd  32993  elrgspnlem4  33177  imaslmod  33305  elrspunidl  33380  rhmpreimaprmidl  33403  qsidomlem1  33404  mxidlprm  33422  1arithidom  33489  dfufd2  33502  extdg1id  33642  pstmxmet  33857  esumfsup  34030  esum2dlem  34052  esum2d  34053  omssubadd  34261  eulerpartlemgvv  34337  signstfvneq0  34533  satffunlem2lem1  35355  matunitlindflem2  37570  aks6d1c2p2  42061  dffltz  42589  eldioph2  42717  limcrecl  45594  icccncfext  45852  ioodvbdlimc1lem2  45897  ioodvbdlimc2lem  45899  stoweidlem60  46025  fourierdlem77  46148  fourierdlem80  46151  fourierdlem103  46174  fourierdlem104  46175  etransclem35  46234