Theorem syl6bi 219

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  ax11i  1647  equveli  1988  eupickbi  2270  2eu2  2285  rgen2a  2681  reu6  3026  sseq0  3583  disjel  3598  disjpss  3602  uneqdifeq  3639  elinti  3936  pwadjoin  4120  preq12b  4128  nnsucelr  4429  sfindbl  4531  funimass2  5171  fconstfv  5457  oprabid  5551  enadj  6061  enpw1  6063  enprmaplem3  6079  nenpw1pwlem2  6086  1cnc  6140  ncspw1eu  6160  ce0nnulb  6183  letc  6232  ncslesuc  6268  nchoicelem3  6292  fnfreclem2  6319  fnfreclem3  6320