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  10488  ccatalpha  11395  fprodntrivap  12367  pwbdvdslemn  12960  isnsgrp  13770  ivthinclemdisj  15790  dvply1  15915  lgseisenlem1  16287  lgsquadlem3  16296  structiedg0val  16379  umgr2edg1  16548  umgr2edgneu  16551  trlsegvdegfi  16806  pwtrufal  17125  pw1nct  17131  nninfsellemsuc  17153