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  4872  elreldm  4893  ssimaex  5625  resflem  5729  f1eqcocnv  5841  fliftfun  5846  isopolem  5872  isosolem  5874  brtposg  6321  issmo2  6356  nnmcl  6548  nnawordi  6582  nnmordi  6583  nnmord  6584  swoord1  6630  ecopovtrn  6700  ecopovtrng  6703  f1domg  6826  mapen  6916  mapxpen  6918  supmoti  7068  isotilem  7081  exmidomniim  7216  enq0tr  7518  prubl  7570  ltexprlemloc  7691  addextpr  7705  recexprlem1ssl  7717  recexprlem1ssu  7718  cauappcvgprlemdisj  7735  mulcmpblnr  7825  mulgt0sr  7862  map2psrprg  7889  ltleletr  8125  ltle  8131  ltadd2  8463  leltadd  8491  reapti  8623  apreap  8631  reapcotr  8642  apcotr  8651  addext  8654  mulext1  8656  zapne  9417  zextle  9434  prime  9442  uzin  9651  indstr  9684  supinfneg  9686  infsupneg  9687  ublbneg  9704  xrltle  9890  xrre2  9913  icc0r  10018  fzrevral  10197  flqge  10389  modqadd1  10470  modqmul1  10486  facdiv  10847  resqrexlemgt0  11202  abs00ap  11244  absext  11245  climshftlemg  11484  climcaucn  11533  dvds2lem  11985  dvdsfac  12042  ltoddhalfle  12075  ndvdsadd  12113  bitsinv1lem  12143  gcdaddm  12176  bezoutlembi  12197  gcdzeq  12214  algcvga  12244  rpdvds  12292  cncongr1  12296  cncongr2  12297  prmind2  12313  euclemma  12339  isprm6  12340  rpexp  12346  sqrt2irr  12355  odzdvds  12439  pclemub  12481  pceulem  12488  pc2dvds  12524  fldivp1  12542  infpnlem1  12553  prmunb  12556  issubg4m  13399  imasabl  13542  fiinbas  14369  bastg  14381  tgcl  14384  opnssneib  14476  tgcnp  14529  iscnp4  14538  cnntr  14545  cnptopresti  14558  lmss  14566  lmtopcnp  14570  txdis  14597  xblss2ps  14724  xblss2  14725  blsscls2  14813  metequiv2  14816  bdxmet  14821  mulc1cncf  14909  cncfco  14911  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  lgsdir  15360  lgsquadlem2  15403  2sqlem8a  15447  2sqlem10  15450  triap  15760