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  3073  opeldmg  4961  elreldm  4983  ssimaex  5738  resflem  5841  f1eqcocnv  5964  fliftfun  5969  isopolem  5995  isosolem  5997  brtposg  6485  issmo2  6520  nnmcl  6714  nnawordi  6748  nnmordi  6749  nnmord  6750  swoord1  6796  ecopovtrn  6866  ecopovtrng  6869  f1domg  6997  mapen  7099  mapxpen  7101  mapunen  7104  supmoti  7284  isotilem  7297  exmidomniim  7432  enq0tr  7749  prubl  7801  ltexprlemloc  7922  addextpr  7936  recexprlem1ssl  7948  recexprlem1ssu  7949  cauappcvgprlemdisj  7966  mulcmpblnr  8056  mulgt0sr  8093  map2psrprg  8120  ltleletr  8355  ltle  8361  ltadd2  8693  leltadd  8721  reapti  8853  apreap  8861  reapcotr  8872  apcotr  8881  addext  8884  mulext1  8886  zapne  9652  zextle  9669  prime  9677  uzin  9887  indstr  9925  supinfneg  9927  infsupneg  9928  ublbneg  9945  xrltle  10131  xrre2  10154  icc0r  10259  fzrevral  10439  flqge  10642  modqadd1  10723  modqmul1  10739  facdiv  11100  elfzelfzccat  11288  resqrexlemgt0  11705  abs00ap  11747  absext  11748  climshftlemg  11987  climcaucn  12036  dvds2lem  12489  dvdsfac  12546  ltoddhalfle  12579  ndvdsadd  12617  bitsinv1lem  12647  gcdaddm  12680  bezoutlembi  12701  gcdzeq  12718  algcvga  12748  rpdvds  12796  cncongr1  12800  cncongr2  12801  prmind2  12817  euclemma  12843  isprm6  12844  rpexp  12850  sqrt2irr  12859  odzdvds  12943  pclemub  12985  pceulem  12992  pc2dvds  13028  fldivp1  13046  infpnlem1  13057  prmunb  13060  issubg4m  13910  imasabl  14053  fiinbas  14914  bastg  14926  tgcl  14929  opnssneib  15021  tgcnp  15074  iscnp4  15083  cnntr  15090  cnptopresti  15103  lmss  15111  lmtopcnp  15115  txdis  15142  xblss2ps  15269  xblss2  15270  blsscls2  15358  metequiv2  15361  bdxmet  15366  mulc1cncf  15454  cncfco  15456  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  lgsdir  15908  lgsquadlem2  15951  2sqlem8a  15995  2sqlem10  15998  uspgrushgr  16175  uspgrupgr  16176  usgruspgr  16178  clwwlkccatlem  16395  triap  16813