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  5704  isoselem  5870  riotass2  5907  oawordriexmid  6537  nnm00  6597  ecopovtrn  6700  ecopovtrng  6703  infglbti  7100  difinfsnlem  7174  enq0tr  7518  addnqprl  7613  addnqpru  7614  mulnqprl  7652  mulnqpru  7653  recexprlemss1l  7719  recexprlemss1u  7720  cauappcvgprlemdisj  7735  mulextsr1lem  7864  pitonn  7932  rereceu  7973  cnegexlem1  8218  ltadd2  8463  eqord2  8528  mulext  8658  mulgt1  8907  lt2halves  9244  addltmul  9245  nzadd  9395  ltsubnn0  9410  zextlt  9435  recnz  9436  zeo  9448  peano5uzti  9451  irradd  9737  irrmul  9738  xltneg  9928  xleadd1  9967  icc0r  10018  fznuz  10194  uznfz  10195  facndiv  10848  rennim  11184  abs00ap  11244  absle  11271  cau3lem  11296  caubnd2  11299  climshft  11486  subcn2  11493  mulcn2  11494  serf0  11534  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  efieq1re  11954  moddvds  11981  dvdsssfz1  12034  nn0seqcvgd  12234  algcvgblem  12242  eucalglt  12250  lcmgcdlem  12270  rpmul  12291  divgcdcoprm0  12294  isprm6  12340  rpexp  12346  eulerthlema  12423  eulerthlemh  12424  prmdiv  12428  pcprendvds2  12485  pcz  12526  pcprmpw  12528  pcadd2  12535  pcfac  12544  expnprm  12547  imasgrp2  13316  issubg4m  13399  znidomb  14290  tgss3  14398  cnpnei  14539  cnntr  14545  hmeoopn  14631  hmeocld  14632  mulcncflem  14927  plycolemc  15078  sincosq3sgn  15148  sincosq4sgn  15149  perfect1  15318  lgsdir2lem4  15356  lgsne0  15363  lgsquad2lem2  15407  2sqlem8a  15447  bj-peano4  15685  iswomni0  15782