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  2045  ceqsalt  2799  sbceqal  3055  csbiebt  3134  rspcsbela  3154  preqr1g  3809  repizf2  4210  copsexg  4292  onun2  4542  suc11g  4609  elrnrexdm  5726  isoselem  5896  riotass2  5933  oawordriexmid  6563  nnm00  6623  ecopovtrn  6726  ecopovtrng  6729  infglbti  7134  difinfsnlem  7208  enq0tr  7554  addnqprl  7649  addnqpru  7650  mulnqprl  7688  mulnqpru  7689  recexprlemss1l  7755  recexprlemss1u  7756  cauappcvgprlemdisj  7771  mulextsr1lem  7900  pitonn  7968  rereceu  8009  cnegexlem1  8254  ltadd2  8499  eqord2  8564  mulext  8694  mulgt1  8943  lt2halves  9280  addltmul  9281  nzadd  9432  ltsubnn0  9447  zextlt  9472  recnz  9473  zeo  9485  peano5uzti  9488  irradd  9774  irrmul  9775  xltneg  9965  xleadd1  10004  icc0r  10055  fznuz  10231  uznfz  10232  facndiv  10891  rennim  11357  abs00ap  11417  absle  11444  cau3lem  11469  caubnd2  11472  climshft  11659  subcn2  11666  mulcn2  11667  serf0  11707  cvgratnnlemnexp  11879  cvgratnnlemmn  11880  efieq1re  12127  moddvds  12154  dvdsssfz1  12207  nn0seqcvgd  12407  algcvgblem  12415  eucalglt  12423  lcmgcdlem  12443  rpmul  12464  divgcdcoprm0  12467  isprm6  12513  rpexp  12519  eulerthlema  12596  eulerthlemh  12597  prmdiv  12601  pcprendvds2  12658  pcz  12699  pcprmpw  12701  pcadd2  12708  pcfac  12717  expnprm  12720  imasgrp2  13490  issubg4m  13573  znidomb  14464  tgss3  14594  cnpnei  14735  cnntr  14741  hmeoopn  14827  hmeocld  14828  mulcncflem  15123  plycolemc  15274  sincosq3sgn  15344  sincosq4sgn  15345  perfect1  15514  lgsdir2lem4  15552  lgsne0  15559  lgsquad2lem2  15603  2sqlem8a  15643  bj-peano4  15965  iswomni0  16064