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  3060  opeldmg  4934  elreldm  4956  ssimaex  5703  resflem  5807  f1eqcocnv  5927  fliftfun  5932  isopolem  5958  isosolem  5960  brtposg  6415  issmo2  6450  nnmcl  6644  nnawordi  6678  nnmordi  6679  nnmord  6680  swoord1  6726  ecopovtrn  6796  ecopovtrng  6799  f1domg  6926  mapen  7027  mapxpen  7029  supmoti  7186  isotilem  7199  exmidomniim  7334  enq0tr  7647  prubl  7699  ltexprlemloc  7820  addextpr  7834  recexprlem1ssl  7846  recexprlem1ssu  7847  cauappcvgprlemdisj  7864  mulcmpblnr  7954  mulgt0sr  7991  map2psrprg  8018  ltleletr  8254  ltle  8260  ltadd2  8592  leltadd  8620  reapti  8752  apreap  8760  reapcotr  8771  apcotr  8780  addext  8783  mulext1  8785  zapne  9547  zextle  9564  prime  9572  uzin  9782  indstr  9820  supinfneg  9822  infsupneg  9823  ublbneg  9840  xrltle  10026  xrre2  10049  icc0r  10154  fzrevral  10333  flqge  10535  modqadd1  10616  modqmul1  10632  facdiv  10993  elfzelfzccat  11170  resqrexlemgt0  11574  abs00ap  11616  absext  11617  climshftlemg  11856  climcaucn  11905  dvds2lem  12357  dvdsfac  12414  ltoddhalfle  12447  ndvdsadd  12485  bitsinv1lem  12515  gcdaddm  12548  bezoutlembi  12569  gcdzeq  12586  algcvga  12616  rpdvds  12664  cncongr1  12668  cncongr2  12669  prmind2  12685  euclemma  12711  isprm6  12712  rpexp  12718  sqrt2irr  12727  odzdvds  12811  pclemub  12853  pceulem  12860  pc2dvds  12896  fldivp1  12914  infpnlem1  12925  prmunb  12928  issubg4m  13773  imasabl  13916  fiinbas  14766  bastg  14778  tgcl  14781  opnssneib  14873  tgcnp  14926  iscnp4  14935  cnntr  14942  cnptopresti  14955  lmss  14963  lmtopcnp  14967  txdis  14994  xblss2ps  15121  xblss2  15122  blsscls2  15210  metequiv2  15213  bdxmet  15218  mulc1cncf  15306  cncfco  15308  sincosq2sgn  15544  sincosq3sgn  15545  sincosq4sgn  15546  lgsdir  15757  lgsquadlem2  15800  2sqlem8a  15844  2sqlem10  15847  uspgrushgr  16024  uspgrupgr  16025  usgruspgr  16027  clwwlkccatlem  16209  triap  16583