Theorem sylnibr 681

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 680	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2519  nssr  3284  difdif  3329  unssin  3443  inssun  3444  undif3ss  3465  ssdif0im  3556  dcun  3601  prneimg  3852  iundif2ss  4031  nssssr  4308  pofun  4403  frirrg  4441  regexmidlem1  4625  dcdifsnid  6658  unfidisj  7092  fidcenumlemrks  7128  difinfsn  7275  pw1nel3  7424  addnqprlemfl  7754  addnqprlemfu  7755  mulnqprlemfl  7770  mulnqprlemfu  7771  cauappcvgprlemladdru  7851  caucvgprprlemaddq  7903  fzpreddisj  10275  fprodntrivap  12103  pw2dvdslemn  12695  isnsgrp  13447  ivthinclemdisj  15322  dvply1  15447  lgseisenlem1  15757  lgsquadlem3  15766  structiedg0val  15849  umgr2edg1  16015  umgr2edgneu  16018  pwtrufal  16389  pw1nct  16395  nninfsellemsuc  16405