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  2047  ceqsalt  2806  sbceqal  3064  csbiebt  3144  rspcsbela  3164  preqr1g  3823  repizf2  4225  copsexg  4309  onun2  4559  suc11g  4626  elrnrexdm  5747  isoselem  5917  riotass2  5956  oawordriexmid  6586  nnm00  6646  ecopovtrn  6749  ecopovtrng  6752  infglbti  7160  difinfsnlem  7234  enq0tr  7589  addnqprl  7684  addnqpru  7685  mulnqprl  7723  mulnqpru  7724  recexprlemss1l  7790  recexprlemss1u  7791  cauappcvgprlemdisj  7806  mulextsr1lem  7935  pitonn  8003  rereceu  8044  cnegexlem1  8289  ltadd2  8534  eqord2  8599  mulext  8729  mulgt1  8978  lt2halves  9315  addltmul  9316  nzadd  9467  ltsubnn0  9482  zextlt  9507  recnz  9508  zeo  9520  peano5uzti  9523  irradd  9809  irrmul  9810  xltneg  10000  xleadd1  10039  icc0r  10090  fznuz  10266  uznfz  10267  facndiv  10928  swrdccatin2  11227  swrdccatin2d  11242  rennim  11479  abs00ap  11539  absle  11566  cau3lem  11591  caubnd2  11594  climshft  11781  subcn2  11788  mulcn2  11789  serf0  11829  cvgratnnlemnexp  12001  cvgratnnlemmn  12002  efieq1re  12249  moddvds  12276  dvdsssfz1  12329  nn0seqcvgd  12529  algcvgblem  12537  eucalglt  12545  lcmgcdlem  12565  rpmul  12586  divgcdcoprm0  12589  isprm6  12635  rpexp  12641  eulerthlema  12718  eulerthlemh  12719  prmdiv  12723  pcprendvds2  12780  pcz  12821  pcprmpw  12823  pcadd2  12830  pcfac  12839  expnprm  12842  imasgrp2  13613  issubg4m  13696  znidomb  14587  tgss3  14717  cnpnei  14858  cnntr  14864  hmeoopn  14950  hmeocld  14951  mulcncflem  15246  plycolemc  15397  sincosq3sgn  15467  sincosq4sgn  15468  perfect1  15637  lgsdir2lem4  15675  lgsne0  15682  lgsquad2lem2  15726  2sqlem8a  15766  bj-peano4  16228  iswomni0  16330