Theorem sylnib 677

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 673	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  678  neqcomd  2209  inssdif0im  3527  undifexmid  4236  ordtriexmidlem2  4567  dmsn0el  5151  fidifsnen  6966  ctssdccl  7212  nninfwlpoimlemginf  7277  onntri35  7348  onntri45  7352  2omotaplemap  7368  exmidapne  7371  ltpopr  7707  caucvgprprlemnbj  7805  xrlttri3  9918  fzneuz  10222  iseqf1olemqcl  10642  iseqf1olemnab  10644  iseqf1olemab  10645  exp3val  10684  pwle2  15897