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  3062  opeldmg  4936  elreldm  4958  ssimaex  5707  resflem  5811  f1eqcocnv  5932  fliftfun  5937  isopolem  5963  isosolem  5965  brtposg  6420  issmo2  6455  nnmcl  6649  nnawordi  6683  nnmordi  6684  nnmord  6685  swoord1  6731  ecopovtrn  6801  ecopovtrng  6804  f1domg  6931  mapen  7032  mapxpen  7034  supmoti  7192  isotilem  7205  exmidomniim  7340  enq0tr  7654  prubl  7706  ltexprlemloc  7827  addextpr  7841  recexprlem1ssl  7853  recexprlem1ssu  7854  cauappcvgprlemdisj  7871  mulcmpblnr  7961  mulgt0sr  7998  map2psrprg  8025  ltleletr  8261  ltle  8267  ltadd2  8599  leltadd  8627  reapti  8759  apreap  8767  reapcotr  8778  apcotr  8787  addext  8790  mulext1  8792  zapne  9554  zextle  9571  prime  9579  uzin  9789  indstr  9827  supinfneg  9829  infsupneg  9830  ublbneg  9847  xrltle  10033  xrre2  10056  icc0r  10161  fzrevral  10340  flqge  10543  modqadd1  10624  modqmul1  10640  facdiv  11001  elfzelfzccat  11181  resqrexlemgt0  11598  abs00ap  11640  absext  11641  climshftlemg  11880  climcaucn  11929  dvds2lem  12382  dvdsfac  12439  ltoddhalfle  12472  ndvdsadd  12510  bitsinv1lem  12540  gcdaddm  12573  bezoutlembi  12594  gcdzeq  12611  algcvga  12641  rpdvds  12689  cncongr1  12693  cncongr2  12694  prmind2  12710  euclemma  12736  isprm6  12737  rpexp  12743  sqrt2irr  12752  odzdvds  12836  pclemub  12878  pceulem  12885  pc2dvds  12921  fldivp1  12939  infpnlem1  12950  prmunb  12953  issubg4m  13798  imasabl  13941  fiinbas  14792  bastg  14804  tgcl  14807  opnssneib  14899  tgcnp  14952  iscnp4  14961  cnntr  14968  cnptopresti  14981  lmss  14989  lmtopcnp  14993  txdis  15020  xblss2ps  15147  xblss2  15148  blsscls2  15236  metequiv2  15239  bdxmet  15244  mulc1cncf  15332  cncfco  15334  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  lgsdir  15783  lgsquadlem2  15826  2sqlem8a  15870  2sqlem10  15873  uspgrushgr  16050  uspgrupgr  16051  usgruspgr  16053  clwwlkccatlem  16270  triap  16684