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  10542  modqadd1  10623  modqmul1  10639  facdiv  11000  elfzelfzccat  11177  resqrexlemgt0  11581  abs00ap  11623  absext  11624  climshftlemg  11863  climcaucn  11912  dvds2lem  12365  dvdsfac  12422  ltoddhalfle  12455  ndvdsadd  12493  bitsinv1lem  12523  gcdaddm  12556  bezoutlembi  12577  gcdzeq  12594  algcvga  12624  rpdvds  12672  cncongr1  12676  cncongr2  12677  prmind2  12693  euclemma  12719  isprm6  12720  rpexp  12726  sqrt2irr  12735  odzdvds  12819  pclemub  12861  pceulem  12868  pc2dvds  12904  fldivp1  12922  infpnlem1  12933  prmunb  12936  issubg4m  13781  imasabl  13924  fiinbas  14775  bastg  14787  tgcl  14790  opnssneib  14882  tgcnp  14935  iscnp4  14944  cnntr  14951  cnptopresti  14964  lmss  14972  lmtopcnp  14976  txdis  15003  xblss2ps  15130  xblss2  15131  blsscls2  15219  metequiv2  15222  bdxmet  15227  mulc1cncf  15315  cncfco  15317  sincosq2sgn  15553  sincosq3sgn  15554  sincosq4sgn  15555  lgsdir  15766  lgsquadlem2  15809  2sqlem8a  15853  2sqlem10  15856  uspgrushgr  16033  uspgrupgr  16034  usgruspgr  16036  clwwlkccatlem  16253  triap  16636