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  4871  elreldm  4892  ssimaex  5622  resflem  5726  f1eqcocnv  5838  fliftfun  5843  isopolem  5869  isosolem  5871  brtposg  6312  issmo2  6347  nnmcl  6539  nnawordi  6573  nnmordi  6574  nnmord  6575  swoord1  6621  ecopovtrn  6691  ecopovtrng  6694  f1domg  6817  mapen  6907  mapxpen  6909  supmoti  7059  isotilem  7072  exmidomniim  7207  enq0tr  7501  prubl  7553  ltexprlemloc  7674  addextpr  7688  recexprlem1ssl  7700  recexprlem1ssu  7701  cauappcvgprlemdisj  7718  mulcmpblnr  7808  mulgt0sr  7845  map2psrprg  7872  ltleletr  8108  ltle  8114  ltadd2  8446  leltadd  8474  reapti  8606  apreap  8614  reapcotr  8625  apcotr  8634  addext  8637  mulext1  8639  zapne  9400  zextle  9417  prime  9425  uzin  9634  indstr  9667  supinfneg  9669  infsupneg  9670  ublbneg  9687  xrltle  9873  xrre2  9896  icc0r  10001  fzrevral  10180  flqge  10372  modqadd1  10453  modqmul1  10469  facdiv  10830  resqrexlemgt0  11185  abs00ap  11227  absext  11228  climshftlemg  11467  climcaucn  11516  dvds2lem  11968  dvdsfac  12025  ltoddhalfle  12058  ndvdsadd  12096  gcdaddm  12151  bezoutlembi  12172  gcdzeq  12189  algcvga  12219  rpdvds  12267  cncongr1  12271  cncongr2  12272  prmind2  12288  euclemma  12314  isprm6  12315  rpexp  12321  sqrt2irr  12330  odzdvds  12414  pclemub  12456  pceulem  12463  pc2dvds  12499  fldivp1  12517  infpnlem1  12528  prmunb  12531  issubg4m  13323  imasabl  13466  fiinbas  14285  bastg  14297  tgcl  14300  opnssneib  14392  tgcnp  14445  iscnp4  14454  cnntr  14461  cnptopresti  14474  lmss  14482  lmtopcnp  14486  txdis  14513  xblss2ps  14640  xblss2  14641  blsscls2  14729  metequiv2  14732  bdxmet  14737  mulc1cncf  14825  cncfco  14827  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  lgsdir  15276  lgsquadlem2  15319  2sqlem8a  15363  2sqlem10  15366  triap  15673