Theorem sylbird 169

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 157	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3d  201  drex1  1733  eqreu  2821  onsucsssucr  4354  ordsucunielexmid  4375  ovi3  5819  tfrlem9  6122  dom2lem  6569  distrlem4prl  7240  distrlem4pru  7241  recexprlemm  7280  caucvgprlem1  7335  caucvgprprlemexb  7363  aptisr  7421  renegcl  7840  addid0  7948  remulext2  8174  mulext1  8186  apmul1  8352  nnge1  8543  0mnnnnn0  8803  nn0lt2  8926  zneo  8946  uzind2  8957  fzind  8960  nn0ind-raph  8962  ledivge1le  9302  elfzmlbp  9692  difelfznle  9695  elfzodifsumelfzo  9761  ssfzo12  9784  flqeqceilz  9874  addmodlteq  9954  uzsinds  9997  facdiv  10261  facwordi  10263  bcpasc  10289  addcn2  10853  mulcn2  10855  climrecvg1n  10891  odd2np1  11300  oddge22np1  11308  gcdaddm  11402  algcvgblem  11458  cncongr1  11512  metss2lem  12283