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  3076  opeldmg  4966  elreldm  4988  ssimaex  5743  resflem  5846  f1eqcocnv  5970  fliftfun  5975  isopolem  6001  isosolem  6003  brtposg  6498  issmo2  6533  nnmcl  6727  nnawordi  6761  nnmordi  6762  nnmord  6763  swoord1  6809  ecopovtrn  6879  ecopovtrng  6882  f1domg  7010  mapen  7112  mapxpen  7114  mapunen  7117  supmoti  7297  isotilem  7310  exmidomniim  7445  enq0tr  7765  prubl  7817  ltexprlemloc  7938  addextpr  7952  recexprlem1ssl  7964  recexprlem1ssu  7965  cauappcvgprlemdisj  7982  mulcmpblnr  8072  mulgt0sr  8109  map2psrprg  8136  ltleletr  8371  ltle  8377  ltadd2  8710  leltadd  8738  reapti  8870  apreap  8878  reapcotr  8889  apcotr  8898  addext  8901  mulext1  8903  zapne  9669  zextle  9687  prime  9695  uzin  9905  indstr  9943  supinfneg  9945  infsupneg  9946  ublbneg  9963  xrltle  10150  xrre2  10173  icc0r  10278  fzrevral  10461  flqge  10666  modqadd1  10747  modqmul1  10763  facdiv  11125  elfzelfzccat  11313  resqrexlemgt0  11730  abs00ap  11772  absext  11773  climshftlemg  12012  climcaucn  12061  dvds2lem  12514  dvdsfac  12571  ltoddhalfle  12604  ndvdsadd  12642  bitsinv1lem  12672  gcdaddm  12705  bezoutlembi  12726  gcdzeq  12743  algcvga  12773  rpdvds  12821  cncongr1  12825  cncongr2  12826  prmind2  12842  euclemma  12868  isprm6  12869  rpexp  12875  sqrt2irr  12884  odzdvds  12968  pclemub  13010  pceulem  13017  pc2dvds  13053  fldivp1  13071  infpnlem1  13082  prmunb  13085  ballotfilem7  13223  issubg4m  13946  imasabl  14089  fiinbas  15040  bastg  15052  tgcl  15055  opnssneib  15147  tgcnp  15200  iscnp4  15209  cnntr  15216  cnptopresti  15229  lmss  15237  lmtopcnp  15241  txdis  15268  xblss2ps  15395  xblss2  15396  blsscls2  15484  metequiv2  15487  bdxmet  15492  mulc1cncf  15580  cncfco  15582  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  lgsdir  16034  lgsquadlem2  16077  2sqlem8a  16121  2sqlem10  16124  uspgrushgr  16301  uspgrupgr  16302  usgruspgr  16304  clwwlkccatlem  16521  triap  16939