Theorem sylibd 149

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

Hypotheses

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

Assertion

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

Proof of Theorem sylibd

Step	Hyp	Ref	Expression
1		sylibd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibd.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	2	biimpd 144	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3d  202  dvelimdf  2069  ceqsalt  2829  sbceqal  3087  csbiebt  3167  rspcsbela  3187  preqr1g  3849  repizf2  4252  copsexg  4336  onun2  4588  suc11g  4655  elrnrexdm  5786  isoselem  5961  riotass2  6000  oawordriexmid  6638  nnm00  6698  ecopovtrn  6801  ecopovtrng  6804  infglbti  7224  difinfsnlem  7298  enq0tr  7654  addnqprl  7749  addnqpru  7750  mulnqprl  7788  mulnqpru  7789  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemdisj  7871  mulextsr1lem  8000  pitonn  8068  rereceu  8109  cnegexlem1  8354  ltadd2  8599  eqord2  8664  mulext  8794  mulgt1  9043  lt2halves  9380  addltmul  9381  nzadd  9532  ltsubnn0  9547  zextlt  9572  recnz  9573  zeo  9585  peano5uzti  9588  irradd  9880  irrmul  9881  xltneg  10071  xleadd1  10110  icc0r  10161  fznuz  10337  uznfz  10338  facndiv  11001  ccatalpha  11190  swrdccatin2  11310  swrdccatin2d  11325  rennim  11563  abs00ap  11623  absle  11650  cau3lem  11675  caubnd2  11678  climshft  11865  subcn2  11872  mulcn2  11873  serf0  11913  cvgratnnlemnexp  12086  cvgratnnlemmn  12087  efieq1re  12334  moddvds  12361  dvdsssfz1  12414  nn0seqcvgd  12614  algcvgblem  12622  eucalglt  12630  lcmgcdlem  12650  rpmul  12671  divgcdcoprm0  12674  isprm6  12720  rpexp  12726  eulerthlema  12803  eulerthlemh  12804  prmdiv  12808  pcprendvds2  12865  pcz  12906  pcprmpw  12908  pcadd2  12915  pcfac  12924  expnprm  12927  imasgrp2  13698  issubg4m  13781  znidomb  14674  tgss3  14804  cnpnei  14945  cnntr  14951  hmeoopn  15037  hmeocld  15038  mulcncflem  15333  plycolemc  15484  sincosq3sgn  15554  sincosq4sgn  15555  perfect1  15724  lgsdir2lem4  15762  lgsne0  15769  lgsquad2lem2  15813  2sqlem8a  15853  clwwlkext2edg  16275  bj-peano4  16553  iswomni0  16658