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-1 5  ax-2 6  ax-mp 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  2870  opeldmg  4654  elreldm  4674  ssimaex  5378  resflem  5476  f1eqcocnv  5584  fliftfun  5589  isopolem  5615  isosolem  5617  brtposg  6033  issmo2  6068  nnmcl  6256  nnawordi  6288  nnmordi  6289  nnmord  6290  swoord1  6335  ecopovtrn  6403  ecopovtrng  6406  f1domg  6529  mapen  6616  mapxpen  6618  supmoti  6742  isotilem  6755  exmidomniim  6858  enq0tr  7054  prubl  7106  ltexprlemloc  7227  addextpr  7241  recexprlem1ssl  7253  recexprlem1ssu  7254  cauappcvgprlemdisj  7271  mulcmpblnr  7348  mulgt0sr  7384  ltleletr  7628  ltle  7633  ltadd2  7958  leltadd  7986  reapti  8117  apreap  8125  reapcotr  8136  apcotr  8145  addext  8148  mulext1  8150  zapne  8882  zextle  8898  prime  8906  uzin  9112  indstr  9142  supinfneg  9144  infsupneg  9145  ublbneg  9159  xrltle  9329  xrre2  9344  icc0r  9405  fzrevral  9580  flqge  9750  modqadd1  9829  modqmul1  9845  facdiv  10207  resqrexlemgt0  10514  abs00ap  10556  absext  10557  climshftlemg  10751  climcaucn  10801  dvds2lem  11147  dvdsfac  11200  ltoddhalfle  11232  ndvdsadd  11270  gcdaddm  11314  bezoutlembi  11333  gcdzeq  11350  algcvga  11372  rpdvds  11420  cncongr1  11424  cncongr2  11425  prmind2  11441  euclemma  11464  isprm6  11465  rpexp  11471  sqrt2irr  11480  fiinbas  11808  bastg  11822  tgcl  11825  mulc1cncf  11918  cncfco  11920