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  3075  opeldmg  4963  elreldm  4985  ssimaex  5740  resflem  5843  f1eqcocnv  5966  fliftfun  5971  isopolem  5997  isosolem  5999  brtposg  6487  issmo2  6522  nnmcl  6716  nnawordi  6750  nnmordi  6751  nnmord  6752  swoord1  6798  ecopovtrn  6868  ecopovtrng  6871  f1domg  6999  mapen  7101  mapxpen  7103  mapunen  7106  supmoti  7286  isotilem  7299  exmidomniim  7434  enq0tr  7754  prubl  7806  ltexprlemloc  7927  addextpr  7941  recexprlem1ssl  7953  recexprlem1ssu  7954  cauappcvgprlemdisj  7971  mulcmpblnr  8061  mulgt0sr  8098  map2psrprg  8125  ltleletr  8360  ltle  8366  ltadd2  8698  leltadd  8726  reapti  8858  apreap  8866  reapcotr  8877  apcotr  8886  addext  8889  mulext1  8891  zapne  9657  zextle  9675  prime  9683  uzin  9893  indstr  9931  supinfneg  9933  infsupneg  9934  ublbneg  9951  xrltle  10137  xrre2  10160  icc0r  10265  fzrevral  10446  flqge  10649  modqadd1  10730  modqmul1  10746  facdiv  11108  elfzelfzccat  11296  resqrexlemgt0  11713  abs00ap  11755  absext  11756  climshftlemg  11995  climcaucn  12044  dvds2lem  12497  dvdsfac  12554  ltoddhalfle  12587  ndvdsadd  12625  bitsinv1lem  12655  gcdaddm  12688  bezoutlembi  12709  gcdzeq  12726  algcvga  12756  rpdvds  12804  cncongr1  12808  cncongr2  12809  prmind2  12825  euclemma  12851  isprm6  12852  rpexp  12858  sqrt2irr  12867  odzdvds  12951  pclemub  12993  pceulem  13000  pc2dvds  13036  fldivp1  13054  infpnlem1  13065  prmunb  13068  issubg4m  13931  imasabl  14074  fiinbas  14963  bastg  14975  tgcl  14978  opnssneib  15070  tgcnp  15123  iscnp4  15132  cnntr  15139  cnptopresti  15152  lmss  15160  lmtopcnp  15164  txdis  15191  xblss2ps  15318  xblss2  15319  blsscls2  15407  metequiv2  15410  bdxmet  15415  mulc1cncf  15503  cncfco  15505  sincosq2sgn  15741  sincosq3sgn  15742  sincosq4sgn  15743  lgsdir  15957  lgsquadlem2  16000  2sqlem8a  16044  2sqlem10  16047  uspgrushgr  16224  uspgrupgr  16225  usgruspgr  16227  clwwlkccatlem  16444  triap  16862