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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3d  202  drex1  1851  eqreu  3018  onsucsssucr  4656  ordsucunielexmid  4678  riotaeqimp  6063  ovi3  6226  suppssrst  6501  suppssrgst  6502  tfrlem9  6590  dom2lem  7058  distrlem4prl  7951  distrlem4pru  7952  recexprlemm  7991  caucvgprlem1  8046  caucvgprprlemexb  8074  aptisr  8146  map2psrprg  8172  renegcl  8587  addid0  8699  remulext2  8929  mulext1  8941  apmul1  9119  nnge1  9328  0mnnnnn0  9597  nn0lt2  9729  zneo  9749  uzind2  9760  fzind  9763  nn0ind-raph  9765  ledivge1le  10129  elfzmlbp  10541  difelfznle  10544  elfzodifsumelfzo  10621  ssfzo12  10644  flqeqceilz  10757  addmodlteq  10837  uzsinds  10883  qsqeqor  11089  facdiv  11178  facwordi  11180  bcpasc  11206  ccatsymb  11372  swrdsbslen  11440  swrdspsleq  11441  swrdlsw  11443  swrdswrdlem  11478  swrdccatin1  11499  pfxccatin12lem3  11506  swrdccat  11509  pfxccat3a  11512  addcn2  12078  mulcn2  12080  climrecvg1n  12116  odd2np1  12642  oddge22np1  12650  bitsfzo  12724  gcdaddm  12763  algcvgblem  12829  cncongr1  12883  pcdvdsb  13101  pcaddlem  13120  infpnlem1  13140  prmunb  13143  imasaddfnlemg  13637  f1ghm0to0  14077  ghmf1  14078  imasring  14371  subrgdvds  14545  aprcotr  14599  quscrng  14872  rnasclassa  15040  metss2lem  15600  pellexlem1  16097  gausslemma2dlem0i  16188  gausslemma2dlem1a  16189  lgseisenlem2  16202  2sqlem6  16251  incistruhgr  16343  wlk1walkdom  16612  wlkv0  16622  clwwlkccatlem  16653