Theorem sylnibr 667

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 666	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 604  ax-in2 605

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexnalim  2455  nssr  3202  difdif  3247  unssin  3361  inssun  3362  undif3ss  3383  ssdif0im  3473  dcun  3519  prneimg  3754  iundif2ss  3931  nssssr  4200  pofun  4290  frirrg  4328  regexmidlem1  4510  dcdifsnid  6472  unfidisj  6887  fidcenumlemrks  6918  difinfsn  7065  pw1nel3  7187  addnqprlemfl  7500  addnqprlemfu  7501  mulnqprlemfl  7516  mulnqprlemfu  7517  cauappcvgprlemladdru  7597  caucvgprprlemaddq  7649  fzpreddisj  10006  fprodntrivap  11525  pw2dvdslemn  12097  ivthinclemdisj  13258  pwtrufal  13877  pw1nct  13883  nninfsellemsuc  13892