Theorem syl6bi 152

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 132	. 2 |- ( ph -> ( ps -> ch ) )
3		syl6bi.2	. 2 |- ( ch -> th )
4	2, 3	syl6 29	1 |- ( ph -> ( ps -> th ) )

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

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  19.33bdc  1521  ax11i  1602  equveli  1642  eupickbi  1982  rgen2a  2375  reu6  2730  sseq0  3258  disjel  3274  disjpss  3278  preq12b  3541  prel12  3542  prneimg  3545  elinti  3624  opthreg  4280  elreldm  4560  issref  4707  relcnvtr  4840  relresfld  4847  funopg  4934  funimass2  4977  fvimacnv  5282  elunirn  5405  oprabid  5537  op1steq  5805  f1o2ndf1  5849  reldmtpos  5868  rntpos  5872  nntri3or  6072  nnaordex  6100  nnawordex  6101  findcard2  6346  findcard2s  6347  lt2addnq  6502  lt2mulnq  6503  genpelvl  6610  genpelvu  6611  distrlem5prl  6684  distrlem5pru  6685  caucvgprlemnkj  6764  rereceu  6963  ltxrlt  7085  0mnnnnn0  8214  elnnnn0b  8226  btwnz  8357  uz11  8495  nn01to3  8552  zq  8561  xrltso  8717  xltnegi  8748  iccleub  8800  fzdcel  8904  uznfz  8965  2ffzeq  8998  elfzonlteqm1  9066  flqeqceilz  9160  frecuzrdgfn  9198  fzfig  9206  caucvgrelemcau  9579  algcvgblem  9888  ialgcvga  9890  bj-elssuniab  9930  bj-nn0sucALT  10103