Theorem sylnibr 684

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2531  nssr  3298  difdif  3344  unssin  3460  inssun  3461  undif3ss  3482  ssdif0im  3573  dcun  3619  prneimg  3878  iundif2ss  4057  nssssr  4338  pofun  4433  frirrg  4471  regexmidlem1  4655  dcdifsnid  6737  elssdc  7162  unfidisj  7182  fidcenumlemrks  7223  difinfsn  7391  pw1nel3  7541  addnqprlemfl  7874  addnqprlemfu  7875  mulnqprlemfl  7890  mulnqprlemfu  7891  cauappcvgprlemladdru  7971  caucvgprprlemaddq  8023  fzpreddisj  10405  ccatalpha  11301  fprodntrivap  12270  pw2dvdslemn  12862  isnsgrp  13619  ivthinclemdisj  15505  dvply1  15630  lgseisenlem1  15943  lgsquadlem3  15952  structiedg0val  16035  umgr2edg1  16204  umgr2edgneu  16207  trlsegvdegfi  16462  pwtrufal  16771  pw1nct  16777  nninfsellemsuc  16790