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  7520  addnqprl  7615  addnqpru  7616  mulnqprl  7654  mulnqpru  7655  recexprlemss1l  7721  recexprlemss1u  7722  cauappcvgprlemdisj  7737  mulextsr1lem  7866  pitonn  7934  rereceu  7975  cnegexlem1  8220  ltadd2  8465  eqord2  8530  mulext  8660  mulgt1  8909  lt2halves  9246  addltmul  9247  nzadd  9397  ltsubnn0  9412  zextlt  9437  recnz  9438  zeo  9450  peano5uzti  9453  irradd  9739  irrmul  9740  xltneg  9930  xleadd1  9969  icc0r  10020  fznuz  10196  uznfz  10197  facndiv  10850  rennim  11186  abs00ap  11246  absle  11273  cau3lem  11298  caubnd2  11301  climshft  11488  subcn2  11495  mulcn2  11496  serf0  11536  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  efieq1re  11956  moddvds  11983  dvdsssfz1  12036  nn0seqcvgd  12236  algcvgblem  12244  eucalglt  12252  lcmgcdlem  12272  rpmul  12293  divgcdcoprm0  12296  isprm6  12342  rpexp  12348  eulerthlema  12425  eulerthlemh  12426  prmdiv  12430  pcprendvds2  12487  pcz  12528  pcprmpw  12530  pcadd2  12537  pcfac  12546  expnprm  12549  imasgrp2  13318  issubg4m  13401  znidomb  14292  tgss3  14400  cnpnei  14541  cnntr  14547  hmeoopn  14633  hmeocld  14634  mulcncflem  14929  plycolemc  15080  sincosq3sgn  15150  sincosq4sgn  15151  perfect1  15320  lgsdir2lem4  15358  lgsne0  15365  lgsquad2lem2  15409  2sqlem8a  15449  bj-peano4  15687  iswomni0  15786