Theorem sylnib 683

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 679	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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnibr  684  neqcomd  2239  inssdif0im  3578  undifexmid  4308  ordtriexmidlem2  4644  dmsn0el  5234  fidifsnen  7127  ctssdccl  7404  nninfwlpoimlemginf  7469  onntri35  7549  onntri45  7553  2omotaplemap  7573  exmidapne  7576  ltpopr  7912  caucvgprprlemnbj  8010  xrlttri3  10133  fzneuz  10439  iseqf1olemqcl  10865  iseqf1olemnab  10867  iseqf1olemab  10868  exp3val  10907  pwle2  16789