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  3059  opeldmg  4928  elreldm  4950  ssimaex  5697  resflem  5801  f1eqcocnv  5921  fliftfun  5926  isopolem  5952  isosolem  5954  brtposg  6406  issmo2  6441  nnmcl  6635  nnawordi  6669  nnmordi  6670  nnmord  6671  swoord1  6717  ecopovtrn  6787  ecopovtrng  6790  f1domg  6917  mapen  7015  mapxpen  7017  supmoti  7168  isotilem  7181  exmidomniim  7316  enq0tr  7629  prubl  7681  ltexprlemloc  7802  addextpr  7816  recexprlem1ssl  7828  recexprlem1ssu  7829  cauappcvgprlemdisj  7846  mulcmpblnr  7936  mulgt0sr  7973  map2psrprg  8000  ltleletr  8236  ltle  8242  ltadd2  8574  leltadd  8602  reapti  8734  apreap  8742  reapcotr  8753  apcotr  8762  addext  8765  mulext1  8767  zapne  9529  zextle  9546  prime  9554  uzin  9763  indstr  9796  supinfneg  9798  infsupneg  9799  ublbneg  9816  xrltle  10002  xrre2  10025  icc0r  10130  fzrevral  10309  flqge  10510  modqadd1  10591  modqmul1  10607  facdiv  10968  elfzelfzccat  11143  resqrexlemgt0  11539  abs00ap  11581  absext  11582  climshftlemg  11821  climcaucn  11870  dvds2lem  12322  dvdsfac  12379  ltoddhalfle  12412  ndvdsadd  12450  bitsinv1lem  12480  gcdaddm  12513  bezoutlembi  12534  gcdzeq  12551  algcvga  12581  rpdvds  12629  cncongr1  12633  cncongr2  12634  prmind2  12650  euclemma  12676  isprm6  12677  rpexp  12683  sqrt2irr  12692  odzdvds  12776  pclemub  12818  pceulem  12825  pc2dvds  12861  fldivp1  12879  infpnlem1  12890  prmunb  12893  issubg4m  13738  imasabl  13881  fiinbas  14731  bastg  14743  tgcl  14746  opnssneib  14838  tgcnp  14891  iscnp4  14900  cnntr  14907  cnptopresti  14920  lmss  14928  lmtopcnp  14932  txdis  14959  xblss2ps  15086  xblss2  15087  blsscls2  15175  metequiv2  15178  bdxmet  15183  mulc1cncf  15271  cncfco  15273  sincosq2sgn  15509  sincosq3sgn  15510  sincosq4sgn  15511  lgsdir  15722  lgsquadlem2  15765  2sqlem8a  15809  2sqlem10  15812  uspgrushgr  15986  uspgrupgr  15987  usgruspgr  15989  triap  16427