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  1989  ceqsalt  2707  sbceqal  2959  csbiebt  3034  rspcsbela  3054  preqr1g  3688  repizf2  4081  copsexg  4161  onun2  4401  suc11g  4467  elrnrexdm  5552  isoselem  5714  riotass2  5749  oawordriexmid  6359  nnm00  6418  ecopovtrn  6519  ecopovtrng  6522  infglbti  6905  difinfsnlem  6977  enq0tr  7235  addnqprl  7330  addnqpru  7331  mulnqprl  7369  mulnqpru  7370  recexprlemss1l  7436  recexprlemss1u  7437  cauappcvgprlemdisj  7452  mulextsr1lem  7581  pitonn  7649  rereceu  7690  cnegexlem1  7930  ltadd2  8174  eqord2  8239  mulext  8369  mulgt1  8614  lt2halves  8948  addltmul  8949  nzadd  9099  zextlt  9136  recnz  9137  zeo  9149  peano5uzti  9152  irradd  9431  irrmul  9432  xltneg  9612  xleadd1  9651  icc0r  9702  fznuz  9875  uznfz  9876  facndiv  10478  rennim  10767  abs00ap  10827  absle  10854  cau3lem  10879  caubnd2  10882  climshft  11066  subcn2  11073  mulcn2  11074  serf0  11114  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  efieq1re  11467  moddvds  11491  dvdsssfz1  11539  nn0seqcvgd  11711  algcvgblem  11719  eucalglt  11727  lcmgcdlem  11747  rpmul  11768  divgcdcoprm0  11771  isprm6  11814  rpexp  11820  tgss3  12236  cnpnei  12377  cnntr  12383  hmeoopn  12469  hmeocld  12470  mulcncflem  12748  sincosq3sgn  12898  sincosq4sgn  12899  bj-peano4  13142