Theorem sylbird 170

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3d  202  drex1  1822  eqreu  2966  onsucsssucr  4561  ordsucunielexmid  4583  ovi3  6090  tfrlem9  6412  dom2lem  6870  distrlem4prl  7704  distrlem4pru  7705  recexprlemm  7744  caucvgprlem1  7799  caucvgprprlemexb  7827  aptisr  7899  map2psrprg  7925  renegcl  8340  addid0  8452  remulext2  8680  mulext1  8692  apmul1  8868  nnge1  9066  0mnnnnn0  9334  nn0lt2  9461  zneo  9481  uzind2  9492  fzind  9495  nn0ind-raph  9497  ledivge1le  9855  elfzmlbp  10261  difelfznle  10264  elfzodifsumelfzo  10337  ssfzo12  10360  flqeqceilz  10470  addmodlteq  10550  uzsinds  10596  qsqeqor  10802  facdiv  10890  facwordi  10892  bcpasc  10918  ccatsymb  11066  swrdsbslen  11127  swrdspsleq  11128  swrdlsw  11130  swrdswrdlem  11163  addcn2  11665  mulcn2  11667  climrecvg1n  11703  odd2np1  12228  oddge22np1  12236  bitsfzo  12310  gcdaddm  12349  algcvgblem  12415  cncongr1  12469  pcdvdsb  12687  pcaddlem  12706  infpnlem1  12726  prmunb  12729  imasaddfnlemg  13190  f1ghm0to0  13652  ghmf1  13653  imasring  13870  subrgdvds  14041  aprcotr  14091  quscrng  14339  metss2lem  15013  gausslemma2dlem0i  15578  gausslemma2dlem1a  15579  lgseisenlem2  15592  2sqlem6  15641  incistruhgr  15730