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  2366  nssr  3073  difdif  3114  unssin  3227  inssun  3228  undif3ss  3249  ssdif0im  3335  prneimg  3601  iundif2ss  3778  nssssr  4023  pofun  4113  frirrg  4151  regexmidlem1  4322  dcdifsnid  6217  unfidisj  6584  addnqprlemfl  7062  addnqprlemfu  7063  mulnqprlemfl  7078  mulnqprlemfu  7079  cauappcvgprlemladdru  7159  caucvgprprlemaddq  7211  fzpreddisj  9415  pw2dvdslemn  11018  nninfsellemsuc  11342