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  3016  opeldmg  4867  elreldm  4888  ssimaex  5618  resflem  5722  f1eqcocnv  5834  fliftfun  5839  isopolem  5865  isosolem  5867  brtposg  6307  issmo2  6342  nnmcl  6534  nnawordi  6568  nnmordi  6569  nnmord  6570  swoord1  6616  ecopovtrn  6686  ecopovtrng  6689  f1domg  6812  mapen  6902  mapxpen  6904  supmoti  7052  isotilem  7065  exmidomniim  7200  enq0tr  7494  prubl  7546  ltexprlemloc  7667  addextpr  7681  recexprlem1ssl  7693  recexprlem1ssu  7694  cauappcvgprlemdisj  7711  mulcmpblnr  7801  mulgt0sr  7838  map2psrprg  7865  ltleletr  8101  ltle  8107  ltadd2  8438  leltadd  8466  reapti  8598  apreap  8606  reapcotr  8617  apcotr  8626  addext  8629  mulext1  8631  zapne  9391  zextle  9408  prime  9416  uzin  9625  indstr  9658  supinfneg  9660  infsupneg  9661  ublbneg  9678  xrltle  9864  xrre2  9887  icc0r  9992  fzrevral  10171  flqge  10351  modqadd1  10432  modqmul1  10448  facdiv  10809  resqrexlemgt0  11164  abs00ap  11206  absext  11207  climshftlemg  11445  climcaucn  11494  dvds2lem  11946  dvdsfac  12002  ltoddhalfle  12034  ndvdsadd  12072  gcdaddm  12121  bezoutlembi  12142  gcdzeq  12159  algcvga  12189  rpdvds  12237  cncongr1  12241  cncongr2  12242  prmind2  12258  euclemma  12284  isprm6  12285  rpexp  12291  sqrt2irr  12300  odzdvds  12383  pclemub  12425  pceulem  12432  pc2dvds  12468  fldivp1  12486  infpnlem1  12497  prmunb  12500  issubg4m  13263  imasabl  13406  fiinbas  14217  bastg  14229  tgcl  14232  opnssneib  14324  tgcnp  14377  iscnp4  14386  cnntr  14393  cnptopresti  14406  lmss  14414  lmtopcnp  14418  txdis  14445  xblss2ps  14572  xblss2  14573  blsscls2  14661  metequiv2  14664  bdxmet  14669  mulc1cncf  14744  cncfco  14746  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  lgsdir  15151  2sqlem8a  15209  2sqlem10  15212  triap  15519