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  1851  eqreu  3018  onsucsssucr  4654  ordsucunielexmid  4676  riotaeqimp  6057  ovi3  6220  suppssrst  6495  suppssrgst  6496  tfrlem9  6584  dom2lem  7052  distrlem4prl  7945  distrlem4pru  7946  recexprlemm  7985  caucvgprlem1  8040  caucvgprprlemexb  8068  aptisr  8140  map2psrprg  8166  renegcl  8581  addid0  8693  remulext2  8922  mulext1  8934  apmul1  9112  nnge1  9310  0mnnnnn0  9578  nn0lt2  9710  zneo  9730  uzind2  9741  fzind  9744  nn0ind-raph  9746  ledivge1le  10110  elfzmlbp  10522  difelfznle  10525  elfzodifsumelfzo  10602  ssfzo12  10625  flqeqceilz  10738  addmodlteq  10818  uzsinds  10864  qsqeqor  11070  facdiv  11159  facwordi  11161  bcpasc  11187  ccatsymb  11353  swrdsbslen  11421  swrdspsleq  11422  swrdlsw  11424  swrdswrdlem  11459  swrdccatin1  11480  pfxccatin12lem3  11487  swrdccat  11490  pfxccat3a  11493  addcn2  12059  mulcn2  12061  climrecvg1n  12097  odd2np1  12623  oddge22np1  12631  bitsfzo  12705  gcdaddm  12744  algcvgblem  12810  cncongr1  12864  pcdvdsb  13082  pcaddlem  13101  infpnlem1  13121  prmunb  13124  imasaddfnlemg  13618  f1ghm0to0  14058  ghmf1  14059  imasring  14352  subrgdvds  14526  aprcotr  14580  quscrng  14853  rnasclassa  15021  metss2lem  15581  pellexlem1  16074  gausslemma2dlem0i  16159  gausslemma2dlem1a  16160  lgseisenlem2  16173  2sqlem6  16222  incistruhgr  16314  wlk1walkdom  16583  wlkv0  16593  clwwlkccatlem  16624