Theorem sylnib 678

Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses

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

Assertion

Ref	Expression
sylnib	|- ( ph -> -. ch )

Proof of Theorem sylnib

Step	Hyp	Ref	Expression
1		sylnib.1	. 2 |- ( ph -> -. ps )
2		sylnib.2	. . 3 |- ( ps <-> ch )
3	2	a1i 9	. 2 |- ( ph -> ( ps <-> ch ) )
4	1, 3	mtbid 674	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnibr  679  neqcomd  2210  inssdif0im  3528  undifexmid  4237  ordtriexmidlem2  4568  dmsn0el  5152  fidifsnen  6967  ctssdccl  7213  nninfwlpoimlemginf  7278  onntri35  7349  onntri45  7353  2omotaplemap  7369  exmidapne  7372  ltpopr  7708  caucvgprprlemnbj  7806  xrlttri3  9919  fzneuz  10223  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemab  10647  exp3val  10686  pwle2  15935