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  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  7171  isotilem  7184  exmidomniim  7319  enq0tr  7632  prubl  7684  ltexprlemloc  7805  addextpr  7819  recexprlem1ssl  7831  recexprlem1ssu  7832  cauappcvgprlemdisj  7849  mulcmpblnr  7939  mulgt0sr  7976  map2psrprg  8003  ltleletr  8239  ltle  8245  ltadd2  8577  leltadd  8605  reapti  8737  apreap  8745  reapcotr  8756  apcotr  8765  addext  8768  mulext1  8770  zapne  9532  zextle  9549  prime  9557  uzin  9767  indstr  9800  supinfneg  9802  infsupneg  9803  ublbneg  9820  xrltle  10006  xrre2  10029  icc0r  10134  fzrevral  10313  flqge  10514  modqadd1  10595  modqmul1  10611  facdiv  10972  elfzelfzccat  11148  resqrexlemgt0  11546  abs00ap  11588  absext  11589  climshftlemg  11828  climcaucn  11877  dvds2lem  12329  dvdsfac  12386  ltoddhalfle  12419  ndvdsadd  12457  bitsinv1lem  12487  gcdaddm  12520  bezoutlembi  12541  gcdzeq  12558  algcvga  12588  rpdvds  12636  cncongr1  12640  cncongr2  12641  prmind2  12657  euclemma  12683  isprm6  12684  rpexp  12690  sqrt2irr  12699  odzdvds  12783  pclemub  12825  pceulem  12832  pc2dvds  12868  fldivp1  12886  infpnlem1  12897  prmunb  12900  issubg4m  13745  imasabl  13888  fiinbas  14738  bastg  14750  tgcl  14753  opnssneib  14845  tgcnp  14898  iscnp4  14907  cnntr  14914  cnptopresti  14927  lmss  14935  lmtopcnp  14939  txdis  14966  xblss2ps  15093  xblss2  15094  blsscls2  15182  metequiv2  15185  bdxmet  15190  mulc1cncf  15278  cncfco  15280  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  lgsdir  15729  lgsquadlem2  15772  2sqlem8a  15816  2sqlem10  15819  uspgrushgr  15993  uspgrupgr  15994  usgruspgr  15996  clwwlkccatlem  16137  triap  16457