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  5931  fliftfun  5936  isopolem  5962  isosolem  5964  brtposg  6419  issmo2  6454  nnmcl  6648  nnawordi  6682  nnmordi  6683  nnmord  6684  swoord1  6730  ecopovtrn  6800  ecopovtrng  6803  f1domg  6930  mapen  7031  mapxpen  7033  supmoti  7191  isotilem  7204  exmidomniim  7339  enq0tr  7653  prubl  7705  ltexprlemloc  7826  addextpr  7840  recexprlem1ssl  7852  recexprlem1ssu  7853  cauappcvgprlemdisj  7870  mulcmpblnr  7960  mulgt0sr  7997  map2psrprg  8024  ltleletr  8260  ltle  8266  ltadd2  8598  leltadd  8626  reapti  8758  apreap  8766  reapcotr  8777  apcotr  8786  addext  8789  mulext1  8791  zapne  9553  zextle  9570  prime  9578  uzin  9788  indstr  9826  supinfneg  9828  infsupneg  9829  ublbneg  9846  xrltle  10032  xrre2  10055  icc0r  10160  fzrevral  10339  flqge  10541  modqadd1  10622  modqmul1  10638  facdiv  10999  elfzelfzccat  11176  resqrexlemgt0  11580  abs00ap  11622  absext  11623  climshftlemg  11862  climcaucn  11911  dvds2lem  12363  dvdsfac  12420  ltoddhalfle  12453  ndvdsadd  12491  bitsinv1lem  12521  gcdaddm  12554  bezoutlembi  12575  gcdzeq  12592  algcvga  12622  rpdvds  12670  cncongr1  12674  cncongr2  12675  prmind2  12691  euclemma  12717  isprm6  12718  rpexp  12724  sqrt2irr  12733  odzdvds  12817  pclemub  12859  pceulem  12866  pc2dvds  12902  fldivp1  12920  infpnlem1  12931  prmunb  12934  issubg4m  13779  imasabl  13922  fiinbas  14772  bastg  14784  tgcl  14787  opnssneib  14879  tgcnp  14932  iscnp4  14941  cnntr  14948  cnptopresti  14961  lmss  14969  lmtopcnp  14973  txdis  15000  xblss2ps  15127  xblss2  15128  blsscls2  15216  metequiv2  15219  bdxmet  15224  mulc1cncf  15312  cncfco  15314  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  lgsdir  15763  lgsquadlem2  15806  2sqlem8a  15850  2sqlem10  15853  uspgrushgr  16030  uspgrupgr  16031  usgruspgr  16033  clwwlkccatlem  16250  triap  16633