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-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  ax11i  1647  equveli  1988  eupickbi  2270  2eu2  2285  rgen2a  2680  reu6  3025  sseq0  3582  disjel  3597  disjpss  3601  uneqdifeq  3638  elinti  3935  pwadjoin  4119  preq12b  4127  nnsucelr  4428  sfindbl  4530  funimass2  5170  fconstfv  5456  oprabid  5550  enadj  6060  enpw1  6062  enprmaplem3  6078  nenpw1pwlem2  6085  1cnc  6139  ncspw1eu  6159  ce0nnulb  6182  letc  6231  ncslesuc  6267  nchoicelem3  6291  fnfreclem2  6318  fnfreclem3  6319