Theorem sylnibr 635

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

Hypotheses

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

Assertion

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

Proof of Theorem sylnibr

Step	Hyp	Ref	Expression
1		sylnibr.1	. 2 |- ( ph -> -. ps )
2		sylnibr.2	. . 3 |- ( ch <-> ps )
3	2	bicomi 130	. 2 |- ( ps <-> ch )
4	1, 3	sylnib 634	1 |- ( ph -> -. ch )

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  rexnalim  2360  nssr  3058  difdif  3098  unssin  3210  inssun  3211  undif3ss  3232  ssdif0im  3315  prneimg  3574  iundif2ss  3751  nssssr  3985  pofun  4075  frirrg  4113  regexmidlem1  4284  nndifsnid  6146  fidifsnid  6406  unfidisj  6442  addnqprlemfl  6811  addnqprlemfu  6812  mulnqprlemfl  6827  mulnqprlemfu  6828  cauappcvgprlemladdru  6908  caucvgprprlemaddq  6960  fzpreddisj  9164  pw2dvdslemn  10687