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  2980  opeldmg  4808  elreldm  4829  ssimaex  5546  resflem  5648  f1eqcocnv  5758  fliftfun  5763  isopolem  5789  isosolem  5791  brtposg  6218  issmo2  6253  nnmcl  6445  nnawordi  6479  nnmordi  6480  nnmord  6481  swoord1  6526  ecopovtrn  6594  ecopovtrng  6597  f1domg  6720  mapen  6808  mapxpen  6810  supmoti  6954  isotilem  6967  exmidomniim  7101  enq0tr  7371  prubl  7423  ltexprlemloc  7544  addextpr  7558  recexprlem1ssl  7570  recexprlem1ssu  7571  cauappcvgprlemdisj  7588  mulcmpblnr  7678  mulgt0sr  7715  map2psrprg  7742  ltleletr  7976  ltle  7982  ltadd2  8313  leltadd  8341  reapti  8473  apreap  8481  reapcotr  8492  apcotr  8501  addext  8504  mulext1  8506  zapne  9261  zextle  9278  prime  9286  uzin  9494  indstr  9527  supinfneg  9529  infsupneg  9530  ublbneg  9547  xrltle  9730  xrre2  9753  icc0r  9858  fzrevral  10036  flqge  10213  modqadd1  10292  modqmul1  10308  facdiv  10647  resqrexlemgt0  10958  abs00ap  11000  absext  11001  climshftlemg  11239  climcaucn  11288  dvds2lem  11739  dvdsfac  11794  ltoddhalfle  11826  ndvdsadd  11864  gcdaddm  11913  bezoutlembi  11934  gcdzeq  11951  algcvga  11979  rpdvds  12027  cncongr1  12031  cncongr2  12032  prmind2  12048  euclemma  12074  isprm6  12075  rpexp  12081  sqrt2irr  12090  odzdvds  12173  pclemub  12215  pceulem  12222  pc2dvds  12257  fldivp1  12274  infpnlem1  12285  prmunb  12288  fiinbas  12647  bastg  12661  tgcl  12664  opnssneib  12756  tgcnp  12809  iscnp4  12818  cnntr  12825  cnptopresti  12838  lmss  12846  lmtopcnp  12850  txdis  12877  xblss2ps  13004  xblss2  13005  blsscls2  13093  metequiv2  13096  bdxmet  13101  mulc1cncf  13176  cncfco  13178  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  lgsdir  13536  2sqlem8a  13558  2sqlem10  13561  triap  13868