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  2016  ceqsalt  2763  sbceqal  3018  csbiebt  3096  rspcsbela  3116  preqr1g  3765  repizf2  4160  copsexg  4242  onun2  4487  suc11g  4554  elrnrexdm  5652  isoselem  5816  riotass2  5852  oawordriexmid  6466  nnm00  6526  ecopovtrn  6627  ecopovtrng  6630  infglbti  7019  difinfsnlem  7093  enq0tr  7428  addnqprl  7523  addnqpru  7524  mulnqprl  7562  mulnqpru  7563  recexprlemss1l  7629  recexprlemss1u  7630  cauappcvgprlemdisj  7645  mulextsr1lem  7774  pitonn  7842  rereceu  7883  cnegexlem1  8126  ltadd2  8370  eqord2  8435  mulext  8565  mulgt1  8814  lt2halves  9148  addltmul  9149  nzadd  9299  ltsubnn0  9314  zextlt  9339  recnz  9340  zeo  9352  peano5uzti  9355  irradd  9640  irrmul  9641  xltneg  9830  xleadd1  9869  icc0r  9920  fznuz  10095  uznfz  10096  facndiv  10710  rennim  11002  abs00ap  11062  absle  11089  cau3lem  11114  caubnd2  11117  climshft  11303  subcn2  11310  mulcn2  11311  serf0  11351  cvgratnnlemnexp  11523  cvgratnnlemmn  11524  efieq1re  11770  moddvds  11797  dvdsssfz1  11848  nn0seqcvgd  12031  algcvgblem  12039  eucalglt  12047  lcmgcdlem  12067  rpmul  12088  divgcdcoprm0  12091  isprm6  12137  rpexp  12143  eulerthlema  12220  eulerthlemh  12221  prmdiv  12225  pcprendvds2  12281  pcz  12321  pcprmpw  12323  pcfac  12338  expnprm  12341  issubg4m  12979  tgss3  13360  cnpnei  13501  cnntr  13507  hmeoopn  13593  hmeocld  13594  mulcncflem  13872  sincosq3sgn  14031  sincosq4sgn  14032  lgsdir2lem4  14214  lgsne0  14221  2sqlem8a  14240  bj-peano4  14478  iswomni0  14570