Theorem sylbida 604

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fzdif1  13652  chnccat  18706  ssdifidlprm  21538  psdmul  22381  efrlim  27187  addsval  28208  mulscan2d  28425  dvdsruasso  33764  fsuppssind  43385  tfsconcat0i  44132  oadif1lem  44166  oadif1  44167  reabsifneg  44418  natglobalincr  47653  f1cof1b  47874  nprmdvdsfacm1lem4  48435  isubgr3stgrlem6  48796  prsthinc  50301