Theorem sylibd 148

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 143	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr3d  201  dvelimdf  1992  ceqsalt  2715  sbceqal  2968  csbiebt  3044  rspcsbela  3064  preqr1g  3701  repizf2  4094  copsexg  4174  onun2  4414  suc11g  4480  elrnrexdm  5567  isoselem  5729  riotass2  5764  oawordriexmid  6374  nnm00  6433  ecopovtrn  6534  ecopovtrng  6537  infglbti  6920  difinfsnlem  6992  enq0tr  7266  addnqprl  7361  addnqpru  7362  mulnqprl  7400  mulnqpru  7401  recexprlemss1l  7467  recexprlemss1u  7468  cauappcvgprlemdisj  7483  mulextsr1lem  7612  pitonn  7680  rereceu  7721  cnegexlem1  7961  ltadd2  8205  eqord2  8270  mulext  8400  mulgt1  8645  lt2halves  8979  addltmul  8980  nzadd  9130  zextlt  9167  recnz  9168  zeo  9180  peano5uzti  9183  irradd  9465  irrmul  9466  xltneg  9649  xleadd1  9688  icc0r  9739  fznuz  9913  uznfz  9914  facndiv  10517  rennim  10806  abs00ap  10866  absle  10893  cau3lem  10918  caubnd2  10921  climshft  11105  subcn2  11112  mulcn2  11113  serf0  11153  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  efieq1re  11514  moddvds  11538  dvdsssfz1  11586  nn0seqcvgd  11758  algcvgblem  11766  eucalglt  11774  lcmgcdlem  11794  rpmul  11815  divgcdcoprm0  11818  isprm6  11861  rpexp  11867  tgss3  12286  cnpnei  12427  cnntr  12433  hmeoopn  12519  hmeocld  12520  mulcncflem  12798  sincosq3sgn  12957  sincosq4sgn  12958  bj-peano4  13324