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  2032  ceqsalt  2786  sbceqal  3042  csbiebt  3121  rspcsbela  3141  preqr1g  3793  repizf2  4192  copsexg  4274  onun2  4523  suc11g  4590  elrnrexdm  5698  isoselem  5864  riotass2  5901  oawordriexmid  6525  nnm00  6585  ecopovtrn  6688  ecopovtrng  6691  infglbti  7086  difinfsnlem  7160  enq0tr  7496  addnqprl  7591  addnqpru  7592  mulnqprl  7630  mulnqpru  7631  recexprlemss1l  7697  recexprlemss1u  7698  cauappcvgprlemdisj  7713  mulextsr1lem  7842  pitonn  7910  rereceu  7951  cnegexlem1  8196  ltadd2  8440  eqord2  8505  mulext  8635  mulgt1  8884  lt2halves  9221  addltmul  9222  nzadd  9372  ltsubnn0  9387  zextlt  9412  recnz  9413  zeo  9425  peano5uzti  9428  irradd  9714  irrmul  9715  xltneg  9905  xleadd1  9944  icc0r  9995  fznuz  10171  uznfz  10172  facndiv  10813  rennim  11149  abs00ap  11209  absle  11236  cau3lem  11261  caubnd2  11264  climshft  11450  subcn2  11457  mulcn2  11458  serf0  11498  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  efieq1re  11918  moddvds  11945  dvdsssfz1  11997  nn0seqcvgd  12182  algcvgblem  12190  eucalglt  12198  lcmgcdlem  12218  rpmul  12239  divgcdcoprm0  12242  isprm6  12288  rpexp  12294  eulerthlema  12371  eulerthlemh  12372  prmdiv  12376  pcprendvds2  12432  pcz  12473  pcprmpw  12475  pcadd2  12482  pcfac  12491  expnprm  12494  imasgrp2  13183  issubg4m  13266  znidomb  14157  tgss3  14257  cnpnei  14398  cnntr  14404  hmeoopn  14490  hmeocld  14491  mulcncflem  14786  plycolemc  14936  sincosq3sgn  15004  sincosq4sgn  15005  lgsdir2lem4  15188  lgsne0  15195  lgsquad2lem2  15239  2sqlem8a  15279  bj-peano4  15517  iswomni0  15611