Theorem sylnibr 601

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 123	. 2 |- (ps <-> ch)
4	1, 3	sylnib 600	1 |- (ph -> -. ch)

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  rexnalim  2311  nssr  2997  difdif  3063  unssin  3170  inssun  3171  undif3ss  3192  ssdif0im  3280  prneimg  3536  iundif2ss  3713  nssssr  3949  pofun  4040  regexmidlem1  4218  addnqprlemfl  6540  addnqprlemfu  6541  cauappcvgprlemladdru  6628  fzpreddisj  8703