Theorem sylibrd 169

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylibrd.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylibrd.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
sylibrd	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibrd.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	biimprd 158	. 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  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr4d  203  sbciegft  3030  opeldmg  4888  elreldm  4909  ssimaex  5647  resflem  5751  f1eqcocnv  5867  fliftfun  5872  isopolem  5898  isosolem  5900  brtposg  6347  issmo2  6382  nnmcl  6574  nnawordi  6608  nnmordi  6609  nnmord  6610  swoord1  6656  ecopovtrn  6726  ecopovtrng  6729  f1domg  6856  mapen  6950  mapxpen  6952  supmoti  7102  isotilem  7115  exmidomniim  7250  enq0tr  7554  prubl  7606  ltexprlemloc  7727  addextpr  7741  recexprlem1ssl  7753  recexprlem1ssu  7754  cauappcvgprlemdisj  7771  mulcmpblnr  7861  mulgt0sr  7898  map2psrprg  7925  ltleletr  8161  ltle  8167  ltadd2  8499  leltadd  8527  reapti  8659  apreap  8667  reapcotr  8678  apcotr  8687  addext  8690  mulext1  8692  zapne  9454  zextle  9471  prime  9479  uzin  9688  indstr  9721  supinfneg  9723  infsupneg  9724  ublbneg  9741  xrltle  9927  xrre2  9950  icc0r  10055  fzrevral  10234  flqge  10432  modqadd1  10513  modqmul1  10529  facdiv  10890  elfzelfzccat  11064  resqrexlemgt0  11375  abs00ap  11417  absext  11418  climshftlemg  11657  climcaucn  11706  dvds2lem  12158  dvdsfac  12215  ltoddhalfle  12248  ndvdsadd  12286  bitsinv1lem  12316  gcdaddm  12349  bezoutlembi  12370  gcdzeq  12387  algcvga  12417  rpdvds  12465  cncongr1  12469  cncongr2  12470  prmind2  12486  euclemma  12512  isprm6  12513  rpexp  12519  sqrt2irr  12528  odzdvds  12612  pclemub  12654  pceulem  12661  pc2dvds  12697  fldivp1  12715  infpnlem1  12726  prmunb  12729  issubg4m  13573  imasabl  13716  fiinbas  14565  bastg  14577  tgcl  14580  opnssneib  14672  tgcnp  14725  iscnp4  14734  cnntr  14741  cnptopresti  14754  lmss  14762  lmtopcnp  14766  txdis  14793  xblss2ps  14920  xblss2  14921  blsscls2  15009  metequiv2  15012  bdxmet  15017  mulc1cncf  15105  cncfco  15107  sincosq2sgn  15343  sincosq3sgn  15344  sincosq4sgn  15345  lgsdir  15556  lgsquadlem2  15599  2sqlem8a  15643  2sqlem10  15646  triap  16042