Theorem sylbida 603

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fzdif1  13629  chnccat  18677  ssdifidlprm  21486  psdmul  22329  efrlim  27134  addsval  28155  mulscan2d  28372  dvdsruasso  33698  fsuppssind  43345  tfsconcat0i  44092  oadif1lem  44126  oadif1  44127  reabsifneg  44378  natglobalincr  47613  f1cof1b  47834  nprmdvdsfacm1lem4  48395  isubgr3stgrlem6  48756  prsthinc  50262