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  2035  ceqsalt  2789  sbceqal  3045  csbiebt  3124  rspcsbela  3144  preqr1g  3797  repizf2  4196  copsexg  4278  onun2  4527  suc11g  4594  elrnrexdm  5702  isoselem  5868  riotass2  5905  oawordriexmid  6530  nnm00  6590  ecopovtrn  6693  ecopovtrng  6696  infglbti  7093  difinfsnlem  7167  enq0tr  7504  addnqprl  7599  addnqpru  7600  mulnqprl  7638  mulnqpru  7639  recexprlemss1l  7705  recexprlemss1u  7706  cauappcvgprlemdisj  7721  mulextsr1lem  7850  pitonn  7918  rereceu  7959  cnegexlem1  8204  ltadd2  8449  eqord2  8514  mulext  8644  mulgt1  8893  lt2halves  9230  addltmul  9231  nzadd  9381  ltsubnn0  9396  zextlt  9421  recnz  9422  zeo  9434  peano5uzti  9437  irradd  9723  irrmul  9724  xltneg  9914  xleadd1  9953  icc0r  10004  fznuz  10180  uznfz  10181  facndiv  10834  rennim  11170  abs00ap  11230  absle  11257  cau3lem  11282  caubnd2  11285  climshft  11472  subcn2  11479  mulcn2  11480  serf0  11520  cvgratnnlemnexp  11692  cvgratnnlemmn  11693  efieq1re  11940  moddvds  11967  dvdsssfz1  12020  nn0seqcvgd  12220  algcvgblem  12228  eucalglt  12236  lcmgcdlem  12256  rpmul  12277  divgcdcoprm0  12280  isprm6  12326  rpexp  12332  eulerthlema  12409  eulerthlemh  12410  prmdiv  12414  pcprendvds2  12471  pcz  12512  pcprmpw  12514  pcadd2  12521  pcfac  12530  expnprm  12533  imasgrp2  13266  issubg4m  13349  znidomb  14240  tgss3  14340  cnpnei  14481  cnntr  14487  hmeoopn  14573  hmeocld  14574  mulcncflem  14869  plycolemc  15020  sincosq3sgn  15090  sincosq4sgn  15091  perfect1  15260  lgsdir2lem4  15298  lgsne0  15305  lgsquad2lem2  15349  2sqlem8a  15389  bj-peano4  15627  iswomni0  15722