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  4364  pofun  4459  frirrg  4497  regexmidlem1  4682  dcdifsnid  6782  elssdc  7215  unfidisj  7235  fidcenumlemrks  7277  difinfsn  7446  pw1nel3  7596  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemfl  7948  mulnqprlemfu  7949  cauappcvgprlemladdru  8029  caucvgprprlemaddq  8081  fzpreddisj  10494  ccatalpha  11402  fprodntrivap  12375  pwbdvdslemn  12968  isnsgrp  13779  gsummptfidmsplit  14253  ivthinclemdisj  15883  dvply1  16008  lgseisenlem1  16411  lgsquadlem3  16420  structiedg0val  16503  umgr2edg1  16672  umgr2edgneu  16675  trlsegvdegfi  16930  pwtrufal  17249  pw1nct  17255  nninfsellemsuc  17278