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  6650  unfidisj  7084  fidcenumlemrks  7120  difinfsn  7267  pw1nel3  7416  addnqprlemfl  7746  addnqprlemfu  7747  mulnqprlemfl  7762  mulnqprlemfu  7763  cauappcvgprlemladdru  7843  caucvgprprlemaddq  7895  fzpreddisj  10267  fprodntrivap  12095  pw2dvdslemn  12687  isnsgrp  13439  ivthinclemdisj  15314  dvply1  15439  lgseisenlem1  15749  lgsquadlem3  15758  structiedg0val  15841  umgr2edg1  16007  umgr2edgneu  16010  pwtrufal  16363  pw1nct  16369  nninfsellemsuc  16378