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  4601  ordsucunielexmid  4623  riotaeqimp  5985  ovi3  6148  tfrlem9  6471  dom2lem  6931  distrlem4prl  7779  distrlem4pru  7780  recexprlemm  7819  caucvgprlem1  7874  caucvgprprlemexb  7902  aptisr  7974  map2psrprg  8000  renegcl  8415  addid0  8527  remulext2  8755  mulext1  8767  apmul1  8943  nnge1  9141  0mnnnnn0  9409  nn0lt2  9536  zneo  9556  uzind2  9567  fzind  9570  nn0ind-raph  9572  ledivge1le  9930  elfzmlbp  10336  difelfznle  10339  elfzodifsumelfzo  10415  ssfzo12  10438  flqeqceilz  10548  addmodlteq  10628  uzsinds  10674  qsqeqor  10880  facdiv  10968  facwordi  10970  bcpasc  10996  ccatsymb  11145  swrdsbslen  11206  swrdspsleq  11207  swrdlsw  11209  swrdswrdlem  11244  swrdccatin1  11265  pfxccatin12lem3  11272  swrdccat  11275  pfxccat3a  11278  addcn2  11829  mulcn2  11831  climrecvg1n  11867  odd2np1  12392  oddge22np1  12400  bitsfzo  12474  gcdaddm  12513  algcvgblem  12579  cncongr1  12633  pcdvdsb  12851  pcaddlem  12870  infpnlem1  12890  prmunb  12893  imasaddfnlemg  13355  f1ghm0to0  13817  ghmf1  13818  imasring  14035  subrgdvds  14207  aprcotr  14257  quscrng  14505  metss2lem  15179  gausslemma2dlem0i  15744  gausslemma2dlem1a  15745  lgseisenlem2  15758  2sqlem6  15807  incistruhgr  15898  wlk1walkdom  16080  wlkv0  16090