Theorem sylbida 598

Description: A syllogism deduction. (Contributed by SN, 16-Jul-2024.)

Hypotheses

Ref	Expression
sylbida.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
sylbida.2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylbida	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem sylbida

Step	Hyp	Ref	Expression
1		sylbida.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpa 477	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		sylbida.2	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
4	2, 3	syldan 597	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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:  fzdif1  13550  chnccat  18583  psdmul  22154  efrlim  26951  addsval  27972  mulscan2d  28189  dvdsruasso  33468  ssdifidlprm  33541  fsuppssind  43043  tfsconcat0i  43790  oadif1lem  43824  oadif1  43825  reabsifneg  44076  natglobalincr  47322  f1cof1b  47540  nprmdvdsfacm1lem4  48101  isubgr3stgrlem6  48462  prsthinc  49954