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  2993  opeldmg  4832  elreldm  4853  ssimaex  5577  resflem  5680  f1eqcocnv  5791  fliftfun  5796  isopolem  5822  isosolem  5824  brtposg  6254  issmo2  6289  nnmcl  6481  nnawordi  6515  nnmordi  6516  nnmord  6517  swoord1  6563  ecopovtrn  6631  ecopovtrng  6634  f1domg  6757  mapen  6845  mapxpen  6847  supmoti  6991  isotilem  7004  exmidomniim  7138  enq0tr  7432  prubl  7484  ltexprlemloc  7605  addextpr  7619  recexprlem1ssl  7631  recexprlem1ssu  7632  cauappcvgprlemdisj  7649  mulcmpblnr  7739  mulgt0sr  7776  map2psrprg  7803  ltleletr  8038  ltle  8044  ltadd2  8375  leltadd  8403  reapti  8535  apreap  8543  reapcotr  8554  apcotr  8563  addext  8566  mulext1  8568  zapne  9326  zextle  9343  prime  9351  uzin  9559  indstr  9592  supinfneg  9594  infsupneg  9595  ublbneg  9612  xrltle  9797  xrre2  9820  icc0r  9925  fzrevral  10104  flqge  10281  modqadd1  10360  modqmul1  10376  facdiv  10717  resqrexlemgt0  11028  abs00ap  11070  absext  11071  climshftlemg  11309  climcaucn  11358  dvds2lem  11809  dvdsfac  11865  ltoddhalfle  11897  ndvdsadd  11935  gcdaddm  11984  bezoutlembi  12005  gcdzeq  12022  algcvga  12050  rpdvds  12098  cncongr1  12102  cncongr2  12103  prmind2  12119  euclemma  12145  isprm6  12146  rpexp  12152  sqrt2irr  12161  odzdvds  12244  pclemub  12286  pceulem  12293  pc2dvds  12328  fldivp1  12345  infpnlem1  12356  prmunb  12359  issubg4m  13051  fiinbas  13519  bastg  13531  tgcl  13534  opnssneib  13626  tgcnp  13679  iscnp4  13688  cnntr  13695  cnptopresti  13708  lmss  13716  lmtopcnp  13720  txdis  13747  xblss2ps  13874  xblss2  13875  blsscls2  13963  metequiv2  13966  bdxmet  13971  mulc1cncf  14046  cncfco  14048  sincosq2sgn  14218  sincosq3sgn  14219  sincosq4sgn  14220  lgsdir  14406  2sqlem8a  14439  2sqlem10  14442  triap  14747