Theorem sylbida 601

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  fzdif1  13611  chnccat  18659  psdmul  22232  efrlim  27035  addsval  28056  mulscan2d  28273  dvdsruasso  33572  ssdifidlprm  33646  fsuppssind  43176  tfsconcat0i  43923  oadif1lem  43957  oadif1  43958  reabsifneg  44209  natglobalincr  47454  f1cof1b  47672  nprmdvdsfacm1lem4  48233  isubgr3stgrlem6  48594  prsthinc  50086