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  3072  opeldmg  4960  elreldm  4982  ssimaex  5737  resflem  5840  f1eqcocnv  5963  fliftfun  5968  isopolem  5994  isosolem  5996  brtposg  6484  issmo2  6519  nnmcl  6713  nnawordi  6747  nnmordi  6748  nnmord  6749  swoord1  6795  ecopovtrn  6865  ecopovtrng  6868  f1domg  6996  mapen  7098  mapxpen  7100  mapunen  7103  supmoti  7283  isotilem  7296  exmidomniim  7431  enq0tr  7745  prubl  7797  ltexprlemloc  7918  addextpr  7932  recexprlem1ssl  7944  recexprlem1ssu  7945  cauappcvgprlemdisj  7962  mulcmpblnr  8052  mulgt0sr  8089  map2psrprg  8116  ltleletr  8351  ltle  8357  ltadd2  8689  leltadd  8717  reapti  8849  apreap  8857  reapcotr  8868  apcotr  8877  addext  8880  mulext1  8882  zapne  9648  zextle  9665  prime  9673  uzin  9883  indstr  9921  supinfneg  9923  infsupneg  9924  ublbneg  9941  xrltle  10127  xrre2  10150  icc0r  10255  fzrevral  10435  flqge  10638  modqadd1  10719  modqmul1  10735  facdiv  11096  elfzelfzccat  11281  resqrexlemgt0  11698  abs00ap  11740  absext  11741  climshftlemg  11980  climcaucn  12029  dvds2lem  12482  dvdsfac  12539  ltoddhalfle  12572  ndvdsadd  12610  bitsinv1lem  12640  gcdaddm  12673  bezoutlembi  12694  gcdzeq  12711  algcvga  12741  rpdvds  12789  cncongr1  12793  cncongr2  12794  prmind2  12810  euclemma  12836  isprm6  12837  rpexp  12843  sqrt2irr  12852  odzdvds  12936  pclemub  12978  pceulem  12985  pc2dvds  13021  fldivp1  13039  infpnlem1  13050  prmunb  13053  issubg4m  13899  imasabl  14042  fiinbas  14901  bastg  14913  tgcl  14916  opnssneib  15008  tgcnp  15061  iscnp4  15070  cnntr  15077  cnptopresti  15090  lmss  15098  lmtopcnp  15102  txdis  15129  xblss2ps  15256  xblss2  15257  blsscls2  15345  metequiv2  15348  bdxmet  15353  mulc1cncf  15441  cncfco  15443  sincosq2sgn  15679  sincosq3sgn  15680  sincosq4sgn  15681  lgsdir  15895  lgsquadlem2  15938  2sqlem8a  15982  2sqlem10  15985  uspgrushgr  16162  uspgrupgr  16163  usgruspgr  16165  clwwlkccatlem  16382  triap  16800