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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr4d  203  sbciegft  3082  opeldmg  4986  elreldm  5008  ssimaex  5764  resflem  5872  f1eqcocnv  5997  fliftfun  6002  isopolem  6028  isosolem  6030  brtposg  6525  issmo2  6560  nnmcl  6754  nnawordi  6788  nnmordi  6789  nnmord  6790  swoord1  6836  ecopovtrn  6906  ecopovtrng  6909  f1domg  7044  mapen  7146  mapxpen  7148  mapunen  7151  supmoti  7334  isotilem  7347  exmidomniim  7482  enq0tr  7802  prubl  7854  ltexprlemloc  7975  addextpr  7989  recexprlem1ssl  8001  recexprlem1ssu  8002  cauappcvgprlemdisj  8019  mulcmpblnr  8109  mulgt0sr  8146  map2psrprg  8173  ltleletr  8408  ltle  8414  ltadd2  8749  leltadd  8777  reapti  8910  apreap  8918  reapcotr  8929  apcotr  8938  addext  8941  mulext1  8943  zapne  9724  zextle  9742  prime  9750  uzin  9965  indstr  10003  supinfneg  10005  infsupneg  10006  ublbneg  10023  xrltle  10211  xrre2  10234  icc0r  10339  fzrevral  10523  flqge  10730  flapge  10731  modqadd1  10813  modqmul1  10829  facdiv  11192  elfzelfzccat  11384  resqrexlemgt0  11802  abs00ap  11844  absext  11845  climshftlemg  12087  climcaucn  12136  dvds2lem  12589  dvdsfac  12646  ltoddhalfle  12679  ndvdsadd  12717  bitsinv1lem  12747  gcdaddm  12780  bezoutlembi  12801  gcdzeq  12818  algcvga  12848  rpdvds  12896  cncongr1  12900  cncongr2  12901  prmind2  12917  euclemma  12944  isprm6  12945  rpexp  12951  sqrt2irr  12960  odzdvds  13047  pclemub  13089  pceulem  13096  pc2dvds  13132  fldivp1  13150  infpnlem1  13161  prmunb  13164  ballotfilem7  13331  issubg4m  14049  imasabl  14224  fiinbas  15249  bastg  15261  tgcl  15264  opnssneib  15356  tgcnp  15409  iscnp4  15418  cnntr  15425  cnptopresti  15438  lmss  15446  lmtopcnp  15450  txdis  15477  xblss2ps  15604  xblss2  15605  blsscls2  15693  metequiv2  15696  bdxmet  15701  mulc1cncf  15789  cncfco  15791  sincosq2sgn  16028  sincosq3sgn  16029  sincosq4sgn  16030  chtublem  16269  chtqub  16270  bposlem1  16285  bposlem3  16287  bposlem7  16291  lgsdir  16333  lgsquadlem2  16376  2sqlem8a  16420  2sqlem10  16423  uspgrushgr  16600  uspgrupgr  16601  usgruspgr  16603  clwwlkccatlem  16820  lealltlt1  16930  lealltlt2  16931  triap  17257