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  3020  opeldmg  4872  elreldm  4893  ssimaex  5623  resflem  5727  f1eqcocnv  5839  fliftfun  5844  isopolem  5870  isosolem  5872  brtposg  6313  issmo2  6348  nnmcl  6540  nnawordi  6574  nnmordi  6575  nnmord  6576  swoord1  6622  ecopovtrn  6692  ecopovtrng  6695  f1domg  6818  mapen  6908  mapxpen  6910  supmoti  7060  isotilem  7073  exmidomniim  7208  enq0tr  7503  prubl  7555  ltexprlemloc  7676  addextpr  7690  recexprlem1ssl  7702  recexprlem1ssu  7703  cauappcvgprlemdisj  7720  mulcmpblnr  7810  mulgt0sr  7847  map2psrprg  7874  ltleletr  8110  ltle  8116  ltadd2  8448  leltadd  8476  reapti  8608  apreap  8616  reapcotr  8627  apcotr  8636  addext  8639  mulext1  8641  zapne  9402  zextle  9419  prime  9427  uzin  9636  indstr  9669  supinfneg  9671  infsupneg  9672  ublbneg  9689  xrltle  9875  xrre2  9898  icc0r  10003  fzrevral  10182  flqge  10374  modqadd1  10455  modqmul1  10471  facdiv  10832  resqrexlemgt0  11187  abs00ap  11229  absext  11230  climshftlemg  11469  climcaucn  11518  dvds2lem  11970  dvdsfac  12027  ltoddhalfle  12060  ndvdsadd  12098  bitsinv1lem  12128  gcdaddm  12161  bezoutlembi  12182  gcdzeq  12199  algcvga  12229  rpdvds  12277  cncongr1  12281  cncongr2  12282  prmind2  12298  euclemma  12324  isprm6  12325  rpexp  12331  sqrt2irr  12340  odzdvds  12424  pclemub  12466  pceulem  12473  pc2dvds  12509  fldivp1  12527  infpnlem1  12538  prmunb  12541  issubg4m  13333  imasabl  13476  fiinbas  14295  bastg  14307  tgcl  14310  opnssneib  14402  tgcnp  14455  iscnp4  14464  cnntr  14471  cnptopresti  14484  lmss  14492  lmtopcnp  14496  txdis  14523  xblss2ps  14650  xblss2  14651  blsscls2  14739  metequiv2  14742  bdxmet  14747  mulc1cncf  14835  cncfco  14837  sincosq2sgn  15073  sincosq3sgn  15074  sincosq4sgn  15075  lgsdir  15286  lgsquadlem2  15329  2sqlem8a  15373  2sqlem10  15376  triap  15683