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  3039  opeldmg  4905  elreldm  4926  ssimaex  5668  resflem  5772  f1eqcocnv  5888  fliftfun  5893  isopolem  5919  isosolem  5921  brtposg  6370  issmo2  6405  nnmcl  6597  nnawordi  6631  nnmordi  6632  nnmord  6633  swoord1  6679  ecopovtrn  6749  ecopovtrng  6752  f1domg  6879  mapen  6975  mapxpen  6977  supmoti  7128  isotilem  7141  exmidomniim  7276  enq0tr  7589  prubl  7641  ltexprlemloc  7762  addextpr  7776  recexprlem1ssl  7788  recexprlem1ssu  7789  cauappcvgprlemdisj  7806  mulcmpblnr  7896  mulgt0sr  7933  map2psrprg  7960  ltleletr  8196  ltle  8202  ltadd2  8534  leltadd  8562  reapti  8694  apreap  8702  reapcotr  8713  apcotr  8722  addext  8725  mulext1  8727  zapne  9489  zextle  9506  prime  9514  uzin  9723  indstr  9756  supinfneg  9758  infsupneg  9759  ublbneg  9776  xrltle  9962  xrre2  9985  icc0r  10090  fzrevral  10269  flqge  10469  modqadd1  10550  modqmul1  10566  facdiv  10927  elfzelfzccat  11101  resqrexlemgt0  11497  abs00ap  11539  absext  11540  climshftlemg  11779  climcaucn  11828  dvds2lem  12280  dvdsfac  12337  ltoddhalfle  12370  ndvdsadd  12408  bitsinv1lem  12438  gcdaddm  12471  bezoutlembi  12492  gcdzeq  12509  algcvga  12539  rpdvds  12587  cncongr1  12591  cncongr2  12592  prmind2  12608  euclemma  12634  isprm6  12635  rpexp  12641  sqrt2irr  12650  odzdvds  12734  pclemub  12776  pceulem  12783  pc2dvds  12819  fldivp1  12837  infpnlem1  12848  prmunb  12851  issubg4m  13696  imasabl  13839  fiinbas  14688  bastg  14700  tgcl  14703  opnssneib  14795  tgcnp  14848  iscnp4  14857  cnntr  14864  cnptopresti  14877  lmss  14885  lmtopcnp  14889  txdis  14916  xblss2ps  15043  xblss2  15044  blsscls2  15132  metequiv2  15135  bdxmet  15140  mulc1cncf  15228  cncfco  15230  sincosq2sgn  15466  sincosq3sgn  15467  sincosq4sgn  15468  lgsdir  15679  lgsquadlem2  15722  2sqlem8a  15766  2sqlem10  15769  uspgrushgr  15943  uspgrupgr  15944  usgruspgr  15946  triap  16308