Theorem sylibrd 168

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 157	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4d  202  sbciegft  2976  opeldmg  4803  elreldm  4824  ssimaex  5541  resflem  5643  f1eqcocnv  5753  fliftfun  5758  isopolem  5784  isosolem  5786  brtposg  6213  issmo2  6248  nnmcl  6440  nnawordi  6474  nnmordi  6475  nnmord  6476  swoord1  6521  ecopovtrn  6589  ecopovtrng  6592  f1domg  6715  mapen  6803  mapxpen  6805  supmoti  6949  isotilem  6962  exmidomniim  7096  enq0tr  7366  prubl  7418  ltexprlemloc  7539  addextpr  7553  recexprlem1ssl  7565  recexprlem1ssu  7566  cauappcvgprlemdisj  7583  mulcmpblnr  7673  mulgt0sr  7710  map2psrprg  7737  ltleletr  7971  ltle  7977  ltadd2  8308  leltadd  8336  reapti  8468  apreap  8476  reapcotr  8487  apcotr  8496  addext  8499  mulext1  8501  zapne  9256  zextle  9273  prime  9281  uzin  9489  indstr  9522  supinfneg  9524  infsupneg  9525  ublbneg  9542  xrltle  9725  xrre2  9748  icc0r  9853  fzrevral  10030  flqge  10207  modqadd1  10286  modqmul1  10302  facdiv  10640  resqrexlemgt0  10948  abs00ap  10990  absext  10991  climshftlemg  11229  climcaucn  11278  dvds2lem  11729  dvdsfac  11783  ltoddhalfle  11815  ndvdsadd  11853  gcdaddm  11902  bezoutlembi  11923  gcdzeq  11940  algcvga  11962  rpdvds  12010  cncongr1  12014  cncongr2  12015  prmind2  12031  euclemma  12055  isprm6  12056  rpexp  12062  sqrt2irr  12071  odzdvds  12154  pclemub  12196  pceulem  12203  pc2dvds  12238  fldivp1  12255  fiinbas  12588  bastg  12602  tgcl  12605  opnssneib  12697  tgcnp  12750  iscnp4  12759  cnntr  12766  cnptopresti  12779  lmss  12787  lmtopcnp  12791  txdis  12818  xblss2ps  12945  xblss2  12946  blsscls2  13034  metequiv2  13037  bdxmet  13042  mulc1cncf  13117  cncfco  13119  sincosq2sgn  13289  sincosq3sgn  13290  sincosq4sgn  13291  triap  13742