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  15241  bastg  15253  tgcl  15256  opnssneib  15348  tgcnp  15401  iscnp4  15410  cnntr  15417  cnptopresti  15430  lmss  15438  lmtopcnp  15442  txdis  15469  xblss2ps  15596  xblss2  15597  blsscls2  15685  metequiv2  15688  bdxmet  15693  mulc1cncf  15781  cncfco  15783  sincosq2sgn  16020  sincosq3sgn  16021  sincosq4sgn  16022  chtublem  16256  chtqub  16257  bposlem1  16272  bposlem3  16274  bposlem7  16278  lgsdir  16320  lgsquadlem2  16363  2sqlem8a  16407  2sqlem10  16410  uspgrushgr  16587  uspgrupgr  16588  usgruspgr  16590  clwwlkccatlem  16807  lealltlt1  16917  lealltlt2  16918  triap  17244