Theorem sylibrd 168

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 157	. 2 |- ( ph -> ( ch -> th ) )
4	1, 3	syld 45	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4d  202  sbciegft  2967  opeldmg  4788  elreldm  4809  ssimaex  5526  resflem  5628  f1eqcocnv  5736  fliftfun  5741  isopolem  5767  isosolem  5769  brtposg  6195  issmo2  6230  nnmcl  6421  nnawordi  6455  nnmordi  6456  nnmord  6457  swoord1  6502  ecopovtrn  6570  ecopovtrng  6573  f1domg  6696  mapen  6784  mapxpen  6786  supmoti  6929  isotilem  6942  exmidomniim  7067  enq0tr  7337  prubl  7389  ltexprlemloc  7510  addextpr  7524  recexprlem1ssl  7536  recexprlem1ssu  7537  cauappcvgprlemdisj  7554  mulcmpblnr  7644  mulgt0sr  7681  map2psrprg  7708  ltleletr  7942  ltle  7947  ltadd2  8277  leltadd  8305  reapti  8437  apreap  8445  reapcotr  8456  apcotr  8465  addext  8468  mulext1  8470  zapne  9221  zextle  9238  prime  9246  uzin  9454  indstr  9487  supinfneg  9489  infsupneg  9490  ublbneg  9504  xrltle  9687  xrre2  9707  icc0r  9812  fzrevral  9989  flqge  10163  modqadd1  10242  modqmul1  10258  facdiv  10594  resqrexlemgt0  10902  abs00ap  10944  absext  10945  climshftlemg  11181  climcaucn  11230  dvds2lem  11680  dvdsfac  11733  ltoddhalfle  11765  ndvdsadd  11803  gcdaddm  11848  bezoutlembi  11869  gcdzeq  11886  algcvga  11908  rpdvds  11956  cncongr1  11960  cncongr2  11961  prmind2  11977  euclemma  12000  isprm6  12001  rpexp  12007  sqrt2irr  12016  fiinbas  12407  bastg  12421  tgcl  12424  opnssneib  12516  tgcnp  12569  iscnp4  12578  cnntr  12585  cnptopresti  12598  lmss  12606  lmtopcnp  12610  txdis  12637  xblss2ps  12764  xblss2  12765  blsscls2  12853  metequiv2  12856  bdxmet  12861  mulc1cncf  12936  cncfco  12938  sincosq2sgn  13108  sincosq3sgn  13109  sincosq4sgn  13110  triap  13562