Theorem syl6bi 161

Description: A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

Hypotheses

Ref	Expression
syl6bi.1	|- ( ph -> ( ps <-> ch ) )
syl6bi.2	|- ( ch -> th )

Assertion

Ref	Expression
syl6bi	|- ( ph -> ( ps -> th ) )

Proof of Theorem syl6bi

Step	Hyp	Ref	Expression
1		syl6bi.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 142	. 2 |- ( ph -> ( ps -> ch ) )
3		syl6bi.2	. 2 |- ( ch -> th )
4	2, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  19.33bdc  1561  ax11i  1642  equveli  1682  eupickbi  2023  rgen2a  2417  reu6  2781  sseq0  3285  disjel  3298  preq12b  3562  prel12  3563  prneimg  3566  elinti  3645  opthreg  4299  elreldm  4578  issref  4727  relcnvtr  4860  relresfld  4867  funopg  4954  funimass2  4997  fvimacnv  5303  elunirn  5426  oprabid  5557  op1steq  5825  f1o2ndf1  5869  reldmtpos  5891  rntpos  5895  nntri3or  6095  nnaordex  6123  nnawordex  6124  findcard2  6373  findcard2s  6374  lt2addnq  6594  lt2mulnq  6595  genpelvl  6702  genpelvu  6703  distrlem5prl  6776  distrlem5pru  6777  caucvgprlemnkj  6856  rereceu  7055  ltxrlt  7178  0mnnnnn0  8320  elnnnn0b  8332  btwnz  8466  uz11  8641  nn01to3  8702  zq  8711  xrltso  8871  xltnegi  8902  iccleub  8954  fzdcel  9059  uznfz  9120  2ffzeq  9151  elfzonlteqm1  9219  flqeqceilz  9320  modqadd1  9363  modqmul1  9379  frecuzrdgfn  9414  fzfig  9422  m1expeven  9523  caucvgrelemcau  9866  rexico  10107  0dvds  10215  alzdvds  10254  opoe  10295  omoe  10296  opeo  10297  omeo  10298  m1exp1  10301  nn0enne  10302  nn0o1gt2  10305  gcdneg  10373  dfgcd2  10403  algcvgblem  10431  ialgcvga  10433  eucalglt  10439  coprmdvds  10474  divgcdcoprmex  10484  cncongr1  10485  prm2orodd  10508  bj-elssuniab  10601  bj-nn0sucALT  10773