Theorem sylnibr 649

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 648	1 |- ( ph -> -. ch )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexnalim  2401  nssr  3123  difdif  3167  unssin  3281  inssun  3282  undif3ss  3303  ssdif0im  3393  dcun  3439  prneimg  3667  iundif2ss  3844  nssssr  4104  pofun  4194  frirrg  4232  regexmidlem1  4408  dcdifsnid  6354  unfidisj  6763  fidcenumlemrks  6793  difinfsn  6937  addnqprlemfl  7315  addnqprlemfu  7316  mulnqprlemfl  7331  mulnqprlemfu  7332  cauappcvgprlemladdru  7412  caucvgprprlemaddq  7464  fzpreddisj  9744  pw2dvdslemn  11688  pwtrufal  12884  nninfsellemsuc  12900