Theorem sylbida 593

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 476	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		sylbida.2	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
4	2, 3	syldan 592	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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:  fzdif1  13535  chnccat  18563  psdmul  22126  efrlim  26952  addsval  27975  mulscan2d  28192  dvdsruasso  33484  ssdifidlprm  33557  fsuppssind  42980  tfsconcat0i  43731  oadif1lem  43765  oadif1  43766  reabsifneg  44017  natglobalincr  47264  f1cof1b  47466  isubgr3stgrlem6  48360  prsthinc  49852