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  2943  opeldmg  4752  elreldm  4773  ssimaex  5490  resflem  5592  f1eqcocnv  5700  fliftfun  5705  isopolem  5731  isosolem  5733  brtposg  6159  issmo2  6194  nnmcl  6385  nnawordi  6419  nnmordi  6420  nnmord  6421  swoord1  6466  ecopovtrn  6534  ecopovtrng  6537  f1domg  6660  mapen  6748  mapxpen  6750  supmoti  6888  isotilem  6901  exmidomniim  7021  enq0tr  7266  prubl  7318  ltexprlemloc  7439  addextpr  7453  recexprlem1ssl  7465  recexprlem1ssu  7466  cauappcvgprlemdisj  7483  mulcmpblnr  7573  mulgt0sr  7610  map2psrprg  7637  ltleletr  7870  ltle  7875  ltadd2  8205  leltadd  8233  reapti  8365  apreap  8373  reapcotr  8384  apcotr  8393  addext  8396  mulext1  8398  cnstab  8431  zapne  9149  zextle  9166  prime  9174  uzin  9382  indstr  9415  supinfneg  9417  infsupneg  9418  ublbneg  9432  xrltle  9614  xrre2  9634  icc0r  9739  fzrevral  9916  flqge  10086  modqadd1  10165  modqmul1  10181  facdiv  10516  resqrexlemgt0  10824  abs00ap  10866  absext  10867  climshftlemg  11103  climcaucn  11152  dvds2lem  11541  dvdsfac  11594  ltoddhalfle  11626  ndvdsadd  11664  gcdaddm  11708  bezoutlembi  11729  gcdzeq  11746  algcvga  11768  rpdvds  11816  cncongr1  11820  cncongr2  11821  prmind2  11837  euclemma  11860  isprm6  11861  rpexp  11867  sqrt2irr  11876  fiinbas  12255  bastg  12269  tgcl  12272  opnssneib  12364  tgcnp  12417  iscnp4  12426  cnntr  12433  cnptopresti  12446  lmss  12454  lmtopcnp  12458  txdis  12485  xblss2ps  12612  xblss2  12613  blsscls2  12701  metequiv2  12704  bdxmet  12709  mulc1cncf  12784  cncfco  12786  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  triap  13399