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  2996  onsucsssucr  4605  ordsucunielexmid  4627  riotaeqimp  5991  ovi3  6154  tfrlem9  6480  dom2lem  6940  distrlem4prl  7797  distrlem4pru  7798  recexprlemm  7837  caucvgprlem1  7892  caucvgprprlemexb  7920  aptisr  7992  map2psrprg  8018  renegcl  8433  addid0  8545  remulext2  8773  mulext1  8785  apmul1  8961  nnge1  9159  0mnnnnn0  9427  nn0lt2  9554  zneo  9574  uzind2  9585  fzind  9588  nn0ind-raph  9590  ledivge1le  9954  elfzmlbp  10360  difelfznle  10363  elfzodifsumelfzo  10439  ssfzo12  10462  flqeqceilz  10573  addmodlteq  10653  uzsinds  10699  qsqeqor  10905  facdiv  10993  facwordi  10995  bcpasc  11021  ccatsymb  11172  swrdsbslen  11240  swrdspsleq  11241  swrdlsw  11243  swrdswrdlem  11278  swrdccatin1  11299  pfxccatin12lem3  11306  swrdccat  11309  pfxccat3a  11312  addcn2  11864  mulcn2  11866  climrecvg1n  11902  odd2np1  12427  oddge22np1  12435  bitsfzo  12509  gcdaddm  12548  algcvgblem  12614  cncongr1  12668  pcdvdsb  12886  pcaddlem  12905  infpnlem1  12925  prmunb  12928  imasaddfnlemg  13390  f1ghm0to0  13852  ghmf1  13853  imasring  14070  subrgdvds  14242  aprcotr  14292  quscrng  14540  metss2lem  15214  gausslemma2dlem0i  15779  gausslemma2dlem1a  15780  lgseisenlem2  15793  2sqlem6  15842  incistruhgr  15934  wlk1walkdom  16170  wlkv0  16180  clwwlkccatlem  16209