Theorem sylnib 687

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 683	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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylnibr  688  neqcomd  2243  inssdif0im  3591  undifexmid  4325  ordtriexmidlem2  4662  dmsn0el  5252  fidifsnen  7162  ctssdccl  7441  nninfwlpoimlemginf  7506  onntri35  7586  onntri45  7590  2omotaplemap  7613  exmidapne  7616  ltpopr  7952  caucvgprprlemnbj  8050  xrlttri3  10178  fzneuz  10486  iseqf1olemqcl  10914  iseqf1olemnab  10916  iseqf1olemab  10917  exp3val  10956  ballotfilemimin  13227  ballotfilemfrcn0  13251  pwle2  16942