Theorem sylnbi 320

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses

Ref	Expression
sylnbi.1	|- ( ph <-> ps )
sylnbi.2	|- ( -. ps -> ch )

Assertion

Ref	Expression
sylnbi	|- ( -. ph -> ch )

Proof of Theorem sylnbi

Step	Hyp	Ref	Expression
1		sylnbi.1	. . 3 |- ( ph <-> ps )
2	1	notbii 310	. 2 |- ( -. ph <-> -. ps )
3		sylnbi.2	. 2 |- ( -. ps -> ch )
4	2, 3	sylbi 207	1 |- ( -. ph -> ch )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  sylnbir  321  reuun2  3910  opswap  5622  iotanul  5866  riotaund  6647  ndmovcom  6821  suppssov1  7327  suppssfv  7331  brtpos  7361  snnen2o  8149  ranklim  8707  rankuni  8726  cdacomen  9003  ituniiun  9244  hashprb  13185  1mavmul  20354  nonbooli  28510  disjunsn  29407  bj-rest10b  33042  ndmaovcl  41283  ndmaovcom  41285  lindslinindsimp1  42246