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  3059  opeldmg  4927  elreldm  4949  ssimaex  5694  resflem  5798  f1eqcocnv  5914  fliftfun  5919  isopolem  5945  isosolem  5947  brtposg  6398  issmo2  6433  nnmcl  6625  nnawordi  6659  nnmordi  6660  nnmord  6661  swoord1  6707  ecopovtrn  6777  ecopovtrng  6780  f1domg  6907  mapen  7003  mapxpen  7005  supmoti  7156  isotilem  7169  exmidomniim  7304  enq0tr  7617  prubl  7669  ltexprlemloc  7790  addextpr  7804  recexprlem1ssl  7816  recexprlem1ssu  7817  cauappcvgprlemdisj  7834  mulcmpblnr  7924  mulgt0sr  7961  map2psrprg  7988  ltleletr  8224  ltle  8230  ltadd2  8562  leltadd  8590  reapti  8722  apreap  8730  reapcotr  8741  apcotr  8750  addext  8753  mulext1  8755  zapne  9517  zextle  9534  prime  9542  uzin  9751  indstr  9784  supinfneg  9786  infsupneg  9787  ublbneg  9804  xrltle  9990  xrre2  10013  icc0r  10118  fzrevral  10297  flqge  10497  modqadd1  10578  modqmul1  10594  facdiv  10955  elfzelfzccat  11130  resqrexlemgt0  11526  abs00ap  11568  absext  11569  climshftlemg  11808  climcaucn  11857  dvds2lem  12309  dvdsfac  12366  ltoddhalfle  12399  ndvdsadd  12437  bitsinv1lem  12467  gcdaddm  12500  bezoutlembi  12521  gcdzeq  12538  algcvga  12568  rpdvds  12616  cncongr1  12620  cncongr2  12621  prmind2  12637  euclemma  12663  isprm6  12664  rpexp  12670  sqrt2irr  12679  odzdvds  12763  pclemub  12805  pceulem  12812  pc2dvds  12848  fldivp1  12866  infpnlem1  12877  prmunb  12880  issubg4m  13725  imasabl  13868  fiinbas  14717  bastg  14729  tgcl  14732  opnssneib  14824  tgcnp  14877  iscnp4  14886  cnntr  14893  cnptopresti  14906  lmss  14914  lmtopcnp  14918  txdis  14945  xblss2ps  15072  xblss2  15073  blsscls2  15161  metequiv2  15164  bdxmet  15169  mulc1cncf  15257  cncfco  15259  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  lgsdir  15708  lgsquadlem2  15751  2sqlem8a  15795  2sqlem10  15798  uspgrushgr  15972  uspgrupgr  15973  usgruspgr  15975  triap  16356