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  2072  ceqsalt  2842  sbceqal  3100  csbiebt  3180  rspcsbela  3200  preqr1g  3872  repizf2  4277  copsexg  4362  onun2  4614  suc11g  4681  elrnrexdm  5818  isoselem  5995  riotass2  6034  oawordriexmid  6705  nnm00  6765  ecopovtrn  6868  ecopovtrng  6871  infglbti  7318  difinfsnlem  7392  enq0tr  7754  addnqprl  7849  addnqpru  7850  mulnqprl  7888  mulnqpru  7889  recexprlemss1l  7955  recexprlemss1u  7956  cauappcvgprlemdisj  7971  mulextsr1lem  8100  pitonn  8168  rereceu  8209  cnegexlem1  8453  ltadd2  8698  eqord2  8763  mulext  8893  mulgt1  9142  lt2halves  9479  addltmul  9480  nzadd  9635  ltsubnn0  9650  zextlt  9676  recnz  9677  zeo  9689  peano5uzti  9692  irradd  9984  irrmul  9985  xltneg  10175  xleadd1  10214  icc0r  10265  fznuz  10443  uznfz  10444  facndiv  11109  ccatalpha  11309  swrdccatin2  11429  swrdccatin2d  11444  rennim  11695  abs00ap  11755  absle  11782  cau3lem  11807  caubnd2  11810  climshft  11997  subcn2  12004  mulcn2  12005  serf0  12045  cvgratnnlemnexp  12218  cvgratnnlemmn  12219  efieq1re  12466  moddvds  12493  dvdsssfz1  12546  nn0seqcvgd  12746  algcvgblem  12754  eucalglt  12762  lcmgcdlem  12782  rpmul  12803  divgcdcoprm0  12806  isprm6  12852  rpexp  12858  eulerthlema  12935  eulerthlemh  12936  prmdiv  12940  pcprendvds2  12997  pcz  13038  pcprmpw  13040  pcadd2  13047  pcfac  13056  expnprm  13059  imasgrp2  13848  issubg4m  13931  znidomb  14855  tgss3  14992  cnpnei  15133  cnntr  15139  hmeoopn  15225  hmeocld  15226  mulcncflem  15521  plycolemc  15672  sincosq3sgn  15742  sincosq4sgn  15743  perfect1  15915  lgsdir2lem4  15953  lgsne0  15960  lgsquad2lem2  16004  2sqlem8a  16044  clwwlkext2edg  16466  bj-peano4  16774  iswomni0  16885