Theorem sylnibr 666

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexnalim  2427  nssr  3157  difdif  3201  unssin  3315  inssun  3316  undif3ss  3337  ssdif0im  3427  dcun  3473  prneimg  3701  iundif2ss  3878  nssssr  4144  pofun  4234  frirrg  4272  regexmidlem1  4448  dcdifsnid  6400  unfidisj  6810  fidcenumlemrks  6841  difinfsn  6985  addnqprlemfl  7367  addnqprlemfu  7368  mulnqprlemfl  7383  mulnqprlemfu  7384  cauappcvgprlemladdru  7464  caucvgprprlemaddq  7516  fzpreddisj  9851  pw2dvdslemn  11843  ivthinclemdisj  12787  pwtrufal  13192  nninfsellemsuc  13208