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  3033  opeldmg  4892  elreldm  4913  ssimaex  5653  resflem  5757  f1eqcocnv  5873  fliftfun  5878  isopolem  5904  isosolem  5906  brtposg  6353  issmo2  6388  nnmcl  6580  nnawordi  6614  nnmordi  6615  nnmord  6616  swoord1  6662  ecopovtrn  6732  ecopovtrng  6735  f1domg  6862  mapen  6958  mapxpen  6960  supmoti  7110  isotilem  7123  exmidomniim  7258  enq0tr  7567  prubl  7619  ltexprlemloc  7740  addextpr  7754  recexprlem1ssl  7766  recexprlem1ssu  7767  cauappcvgprlemdisj  7784  mulcmpblnr  7874  mulgt0sr  7911  map2psrprg  7938  ltleletr  8174  ltle  8180  ltadd2  8512  leltadd  8540  reapti  8672  apreap  8680  reapcotr  8691  apcotr  8700  addext  8703  mulext1  8705  zapne  9467  zextle  9484  prime  9492  uzin  9701  indstr  9734  supinfneg  9736  infsupneg  9737  ublbneg  9754  xrltle  9940  xrre2  9963  icc0r  10068  fzrevral  10247  flqge  10447  modqadd1  10528  modqmul1  10544  facdiv  10905  elfzelfzccat  11079  resqrexlemgt0  11406  abs00ap  11448  absext  11449  climshftlemg  11688  climcaucn  11737  dvds2lem  12189  dvdsfac  12246  ltoddhalfle  12279  ndvdsadd  12317  bitsinv1lem  12347  gcdaddm  12380  bezoutlembi  12401  gcdzeq  12418  algcvga  12448  rpdvds  12496  cncongr1  12500  cncongr2  12501  prmind2  12517  euclemma  12543  isprm6  12544  rpexp  12550  sqrt2irr  12559  odzdvds  12643  pclemub  12685  pceulem  12692  pc2dvds  12728  fldivp1  12746  infpnlem1  12757  prmunb  12760  issubg4m  13604  imasabl  13747  fiinbas  14596  bastg  14608  tgcl  14611  opnssneib  14703  tgcnp  14756  iscnp4  14765  cnntr  14772  cnptopresti  14785  lmss  14793  lmtopcnp  14797  txdis  14824  xblss2ps  14951  xblss2  14952  blsscls2  15040  metequiv2  15043  bdxmet  15048  mulc1cncf  15136  cncfco  15138  sincosq2sgn  15374  sincosq3sgn  15375  sincosq4sgn  15376  lgsdir  15587  lgsquadlem2  15630  2sqlem8a  15674  2sqlem10  15677  triap  16109