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  3063  opeldmg  4942  elreldm  4964  ssimaex  5716  resflem  5819  f1eqcocnv  5942  fliftfun  5947  isopolem  5973  isosolem  5975  brtposg  6463  issmo2  6498  nnmcl  6692  nnawordi  6726  nnmordi  6727  nnmord  6728  swoord1  6774  ecopovtrn  6844  ecopovtrng  6847  f1domg  6974  mapen  7075  mapxpen  7077  supmoti  7235  isotilem  7248  exmidomniim  7383  enq0tr  7697  prubl  7749  ltexprlemloc  7870  addextpr  7884  recexprlem1ssl  7896  recexprlem1ssu  7897  cauappcvgprlemdisj  7914  mulcmpblnr  8004  mulgt0sr  8041  map2psrprg  8068  ltleletr  8303  ltle  8309  ltadd2  8641  leltadd  8669  reapti  8801  apreap  8809  reapcotr  8820  apcotr  8829  addext  8832  mulext1  8834  zapne  9598  zextle  9615  prime  9623  uzin  9833  indstr  9871  supinfneg  9873  infsupneg  9874  ublbneg  9891  xrltle  10077  xrre2  10100  icc0r  10205  fzrevral  10385  flqge  10588  modqadd1  10669  modqmul1  10685  facdiv  11046  elfzelfzccat  11226  resqrexlemgt0  11643  abs00ap  11685  absext  11686  climshftlemg  11925  climcaucn  11974  dvds2lem  12427  dvdsfac  12484  ltoddhalfle  12517  ndvdsadd  12555  bitsinv1lem  12585  gcdaddm  12618  bezoutlembi  12639  gcdzeq  12656  algcvga  12686  rpdvds  12734  cncongr1  12738  cncongr2  12739  prmind2  12755  euclemma  12781  isprm6  12782  rpexp  12788  sqrt2irr  12797  odzdvds  12881  pclemub  12923  pceulem  12930  pc2dvds  12966  fldivp1  12984  infpnlem1  12995  prmunb  12998  issubg4m  13843  imasabl  13986  fiinbas  14843  bastg  14855  tgcl  14858  opnssneib  14950  tgcnp  15003  iscnp4  15012  cnntr  15019  cnptopresti  15032  lmss  15040  lmtopcnp  15044  txdis  15071  xblss2ps  15198  xblss2  15199  blsscls2  15287  metequiv2  15290  bdxmet  15295  mulc1cncf  15383  cncfco  15385  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  lgsdir  15837  lgsquadlem2  15880  2sqlem8a  15924  2sqlem10  15927  uspgrushgr  16104  uspgrupgr  16105  usgruspgr  16107  clwwlkccatlem  16324  triap  16744