Theorem sylbird 168

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3imtr3d  200  drex1  1719  eqreu  2784  onsucsssucr  4253  ordsucunielexmid  4274  ovi3  5657  tfrlem9  5958  rdgon  5996  dom2lem  6275  distrlem4prl  6774  distrlem4pru  6775  recexprlemm  6814  caucvgprlem1  6869  caucvgprprlemexb  6897  aptisr  6955  renegcl  7369  addid0  7477  remulext2  7700  mulext1  7712  apmul1  7876  nnge1  8062  0mnnnnn0  8320  nn0lt2  8429  zneo  8448  uzind2  8459  fzind  8462  nn0ind-raph  8464  ledivge1le  8803  elfzmlbp  9143  difelfznle  9146  elfzodifsumelfzo  9210  ssfzo12  9233  flqeqceilz  9320  addmodlteq  9400  uzsinds  9428  facdiv  9665  facwordi  9667  bcpasc  9693  addcn2  10149  mulcn2  10151  climrecvg1n  10185  odd2np1  10272  oddge22np1  10281  gcdaddm  10375  algcvgblem  10431  cncongr1  10485