Theorem sylnibr 688

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

This proof depends on syntax axioms:   -. wn 3   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  rexnalim  2539  nssr  3308  difdif  3354  unssin  3470  inssun  3471  undif3ss  3492  ssdif0im  3589  dcun  3637  prneimg  3899  iundif2ss  4078  nssssr  4362  pofun  4457  frirrg  4495  regexmidlem1  4680  dcdifsnid  6777  elssdc  7209  unfidisj  7229  fidcenumlemrks  7270  difinfsn  7440  pw1nel3  7590  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemfl  7942  mulnqprlemfu  7943  cauappcvgprlemladdru  8023  caucvgprprlemaddq  8075  fzpreddisj  10478  ccatalpha  11381  fprodntrivap  12351  pw2dvdslemn  12943  isnsgrp  13721  ivthinclemdisj  15741  dvply1  15866  lgseisenlem1  16189  lgsquadlem3  16198  structiedg0val  16281  umgr2edg1  16450  umgr2edgneu  16453  trlsegvdegfi  16708  pwtrufal  17027  pw1nct  17033  nninfsellemsuc  17055