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  2067  ceqsalt  2827  sbceqal  3085  csbiebt  3165  rspcsbela  3185  preqr1g  3847  repizf2  4250  copsexg  4334  onun2  4586  suc11g  4653  elrnrexdm  5782  isoselem  5956  riotass2  5995  oawordriexmid  6633  nnm00  6693  ecopovtrn  6796  ecopovtrng  6799  infglbti  7218  difinfsnlem  7292  enq0tr  7647  addnqprl  7742  addnqpru  7743  mulnqprl  7781  mulnqpru  7782  recexprlemss1l  7848  recexprlemss1u  7849  cauappcvgprlemdisj  7864  mulextsr1lem  7993  pitonn  8061  rereceu  8102  cnegexlem1  8347  ltadd2  8592  eqord2  8657  mulext  8787  mulgt1  9036  lt2halves  9373  addltmul  9374  nzadd  9525  ltsubnn0  9540  zextlt  9565  recnz  9566  zeo  9578  peano5uzti  9581  irradd  9873  irrmul  9874  xltneg  10064  xleadd1  10103  icc0r  10154  fznuz  10330  uznfz  10331  facndiv  10994  ccatalpha  11183  swrdccatin2  11303  swrdccatin2d  11318  rennim  11556  abs00ap  11616  absle  11643  cau3lem  11668  caubnd2  11671  climshft  11858  subcn2  11865  mulcn2  11866  serf0  11906  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  efieq1re  12326  moddvds  12353  dvdsssfz1  12406  nn0seqcvgd  12606  algcvgblem  12614  eucalglt  12622  lcmgcdlem  12642  rpmul  12663  divgcdcoprm0  12666  isprm6  12712  rpexp  12718  eulerthlema  12795  eulerthlemh  12796  prmdiv  12800  pcprendvds2  12857  pcz  12898  pcprmpw  12900  pcadd2  12907  pcfac  12916  expnprm  12919  imasgrp2  13690  issubg4m  13773  znidomb  14665  tgss3  14795  cnpnei  14936  cnntr  14942  hmeoopn  15028  hmeocld  15029  mulcncflem  15324  plycolemc  15475  sincosq3sgn  15545  sincosq4sgn  15546  perfect1  15715  lgsdir2lem4  15753  lgsne0  15760  lgsquad2lem2  15804  2sqlem8a  15844  clwwlkext2edg  16231  bj-peano4  16500  iswomni0  16605