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  2072  ceqsalt  2842  sbceqal  3101  csbiebt  3181  rspcsbela  3201  preqr1g  3875  repizf2  4280  copsexg  4365  onun2  4617  suc11g  4684  elrnrexdm  5821  isoselem  5999  riotass2  6040  oawordriexmid  6716  nnm00  6776  ecopovtrn  6879  ecopovtrng  6882  infglbti  7329  difinfsnlem  7403  enq0tr  7765  addnqprl  7860  addnqpru  7861  mulnqprl  7899  mulnqpru  7900  recexprlemss1l  7966  recexprlemss1u  7967  cauappcvgprlemdisj  7982  mulextsr1lem  8111  pitonn  8179  rereceu  8220  cnegexlem1  8465  ltadd2  8711  eqord2  8776  mulext  8906  mulgt1  9157  lt2halves  9494  addltmul  9495  nzadd  9650  ltsubnn0  9665  zextlt  9691  recnz  9692  zeo  9704  peano5uzti  9707  irradd  9999  irrmul  10000  xltneg  10191  xleadd1  10230  icc0r  10281  fznuz  10461  uznfz  10462  facndiv  11129  ccatalpha  11329  swrdccatin2  11449  swrdccatin2d  11464  rennim  11715  abs00ap  11775  absle  11802  cau3lem  11827  caubnd2  11830  climshft  12017  subcn2  12024  mulcn2  12025  serf0  12065  cvgratnnlemnexp  12238  cvgratnnlemmn  12239  efieq1re  12486  moddvds  12513  dvdsssfz1  12566  nn0seqcvgd  12766  algcvgblem  12774  eucalglt  12782  lcmgcdlem  12802  rpmul  12823  divgcdcoprm0  12826  isprm6  12872  rpexp  12878  eulerthlema  12955  eulerthlemh  12956  prmdiv  12960  pcprendvds2  13017  pcz  13058  pcprmpw  13060  pcadd2  13067  pcfac  13076  expnprm  13079  imasgrp2  13866  issubg4m  13949  znidomb  14935  tgss3  15072  cnpnei  15213  cnntr  15219  hmeoopn  15305  hmeocld  15306  mulcncflem  15601  plycolemc  15752  sincosq3sgn  15822  sincosq4sgn  15823  perfect1  15995  lgsdir2lem4  16033  lgsne0  16040  lgsquad2lem2  16084  2sqlem8a  16124  clwwlkext2edg  16546  bj-peano4  16864  iswomni0  16975