Theorem sylbid 139

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
sylbid.2	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylbid	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylbid

Step	Hyp	Ref	Expression
1		sylbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 132	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbid.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 40	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3imtr4d  192  nlimsucg  4290  poltletr  4725  xp11m  4759  fvmptdf  5258  eusvobj2  5498  ovmpt2df  5632  f1o2ndf1  5849  smoiso  5917  nnsseleq  6079  ecopovtrn  6203  ecopovtrng  6206  dom2lem  6252  fundmen  6286  fidifsnen  6331  findcard2  6346  findcard2s  6347  ordiso2  6357  addcanpig  6432  mulcanpig  6433  addnidpig  6434  ordpipqqs  6472  ltexnqq  6506  prarloclemlo  6592  genpcdl  6617  genpcuu  6618  mulnqprl  6666  mulnqpru  6667  distrlem1prl  6680  distrlem1pru  6681  distrlem4prl  6682  distrlem4pru  6683  distrlem5prl  6684  distrlem5pru  6685  ltsopr  6694  ltexprlemfl  6707  ltexprlemfu  6709  recexprlemss1l  6733  recexprlemss1u  6734  aptiprleml  6737  ltsrprg  6832  lttrsr  6847  mulextsr1lem  6864  axapti  7090  cnegexlem1  7186  le2add  7439  lt2add  7440  ltleadd  7441  lt2sub  7455  le2sub  7456  recexre  7569  reapti  7570  apreap  7578  reapcotr  7589  remulext1  7590  apreim  7594  apcotr  7598  mulext2  7604  recexap  7634  addltmul  8161  elnnz  8255  zleloe  8292  nn0n0n1ge2b  8320  nn0lt2  8322  zextlt  8332  uzind2  8350  eluzdc  8547  qreccl  8576  xltnegi  8748  iccid  8794  icoshft  8858  fzofzim  9044  flqeqceilz  9160  frec2uzrand  9191  frecuzrdgfn  9198  recvguniq  9593  abs00ap  9660  absext  9661  absnid  9671  cau3lem  9710  climuni  9814  2clim  9822  algcvgblem  9888  ialgcvga  9890