Theorem sylibrd 169

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylibrd.1	|- ( ph -> ( ps -> ch ) )
sylibrd.2	|- ( ph -> ( th <-> ch ) )

Assertion

Ref	Expression
sylibrd	|- ( ph -> ( ps -> th ) )

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 |- ( ph -> ( ps -> ch ) )
2		sylibrd.2	. . 3 |- ( ph -> ( th <-> ch ) )
3	2	biimprd 158	. 2 |- ( ph -> ( ch -> th ) )
4	1, 3	syld 45	1 |- ( ph -> ( ps -> th ) )

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  7183  isotilem  7196  exmidomniim  7331  enq0tr  7644  prubl  7696  ltexprlemloc  7817  addextpr  7831  recexprlem1ssl  7843  recexprlem1ssu  7844  cauappcvgprlemdisj  7861  mulcmpblnr  7951  mulgt0sr  7988  map2psrprg  8015  ltleletr  8251  ltle  8257  ltadd2  8589  leltadd  8617  reapti  8749  apreap  8757  reapcotr  8768  apcotr  8777  addext  8780  mulext1  8782  zapne  9544  zextle  9561  prime  9569  uzin  9779  indstr  9817  supinfneg  9819  infsupneg  9820  ublbneg  9837  xrltle  10023  xrre2  10046  icc0r  10151  fzrevral  10330  flqge  10532  modqadd1  10613  modqmul1  10629  facdiv  10990  elfzelfzccat  11167  resqrexlemgt0  11571  abs00ap  11613  absext  11614  climshftlemg  11853  climcaucn  11902  dvds2lem  12354  dvdsfac  12411  ltoddhalfle  12444  ndvdsadd  12482  bitsinv1lem  12512  gcdaddm  12545  bezoutlembi  12566  gcdzeq  12583  algcvga  12613  rpdvds  12661  cncongr1  12665  cncongr2  12666  prmind2  12682  euclemma  12708  isprm6  12709  rpexp  12715  sqrt2irr  12724  odzdvds  12808  pclemub  12850  pceulem  12857  pc2dvds  12893  fldivp1  12911  infpnlem1  12922  prmunb  12925  issubg4m  13770  imasabl  13913  fiinbas  14763  bastg  14775  tgcl  14778  opnssneib  14870  tgcnp  14923  iscnp4  14932  cnntr  14939  cnptopresti  14952  lmss  14960  lmtopcnp  14964  txdis  14991  xblss2ps  15118  xblss2  15119  blsscls2  15207  metequiv2  15210  bdxmet  15215  mulc1cncf  15303  cncfco  15305  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  lgsdir  15754  lgsquadlem2  15797  2sqlem8a  15841  2sqlem10  15844  uspgrushgr  16019  uspgrupgr  16020  usgruspgr  16022  clwwlkccatlem  16195  triap  16569