Theorem sylnib 680

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 676	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnibr  681  neqcomd  2234  inssdif0im  3560  undifexmid  4281  ordtriexmidlem2  4616  dmsn0el  5204  fidifsnen  7052  ctssdccl  7301  nninfwlpoimlemginf  7366  onntri35  7445  onntri45  7449  2omotaplemap  7466  exmidapne  7469  ltpopr  7805  caucvgprprlemnbj  7903  xrlttri3  10022  fzneuz  10326  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemab  10754  exp3val  10793  pwle2  16535