Theorem sylbird 159

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

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

Assertion

Ref	Expression
sylbird	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylbird

Step	Hyp	Ref	Expression
1		sylbird.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 147	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 40	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3imtr3d  191  drex1  1679  eqreu  2733  onsucsssucr  4235  ordsucunielexmid  4256  ovi3  5637  tfrlem9  5935  rdgon  5973  dom2lem  6252  distrlem4prl  6682  distrlem4pru  6683  recexprlemm  6722  caucvgprlem1  6777  caucvgprprlemexb  6805  aptisr  6863  renegcl  7272  remulext2  7591  mulext1  7603  apmul1  7764  nnge1  7937  0mnnnnn0  8214  nn0lt2  8322  zneo  8339  uzind2  8350  fzind  8353  nn0ind-raph  8355  ledivge1le  8652  elfzmlbp  8990  difelfznle  8993  elfzodifsumelfzo  9057  ssfzo12  9080  flqeqceilz  9160  addcn2  9831  mulcn2  9833  climrecvg1n  9867  algcvgblem  9888