Theorem sylnib 665

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 661	1 |- ( ph -> -. ch )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylnibr  666  neqcomd  2144  inssdif0im  3430  undifexmid  4117  ordtriexmidlem2  4436  dmsn0el  5008  fidifsnen  6764  ctssdccl  6996  ltpopr  7403  caucvgprprlemnbj  7501  xrlttri3  9583  fzneuz  9881  iseqf1olemqcl  10259  iseqf1olemnab  10261  iseqf1olemab  10262  exp3val  10295  pwle2  13193