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  1844  eqreu  2995  onsucsssucr  4602  ordsucunielexmid  4624  riotaeqimp  5988  ovi3  6151  tfrlem9  6476  dom2lem  6936  distrlem4prl  7787  distrlem4pru  7788  recexprlemm  7827  caucvgprlem1  7882  caucvgprprlemexb  7910  aptisr  7982  map2psrprg  8008  renegcl  8423  addid0  8535  remulext2  8763  mulext1  8775  apmul1  8951  nnge1  9149  0mnnnnn0  9417  nn0lt2  9544  zneo  9564  uzind2  9575  fzind  9578  nn0ind-raph  9580  ledivge1le  9939  elfzmlbp  10345  difelfznle  10348  elfzodifsumelfzo  10424  ssfzo12  10447  flqeqceilz  10557  addmodlteq  10637  uzsinds  10683  qsqeqor  10889  facdiv  10977  facwordi  10979  bcpasc  11005  ccatsymb  11155  swrdsbslen  11219  swrdspsleq  11220  swrdlsw  11222  swrdswrdlem  11257  swrdccatin1  11278  pfxccatin12lem3  11285  swrdccat  11288  pfxccat3a  11291  addcn2  11842  mulcn2  11844  climrecvg1n  11880  odd2np1  12405  oddge22np1  12413  bitsfzo  12487  gcdaddm  12526  algcvgblem  12592  cncongr1  12646  pcdvdsb  12864  pcaddlem  12883  infpnlem1  12903  prmunb  12906  imasaddfnlemg  13368  f1ghm0to0  13830  ghmf1  13831  imasring  14048  subrgdvds  14220  aprcotr  14270  quscrng  14518  metss2lem  15192  gausslemma2dlem0i  15757  gausslemma2dlem1a  15758  lgseisenlem2  15771  2sqlem6  15820  incistruhgr  15911  wlk1walkdom  16131  wlkv0  16141  clwwlkccatlem  16169