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  elssdc  7075  unfidisj  7095  fidcenumlemrks  7131  difinfsn  7278  pw1nel3  7427  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemfl  7773  mulnqprlemfu  7774  cauappcvgprlemladdru  7854  caucvgprprlemaddq  7906  fzpreddisj  10279  ccatalpha  11161  fprodntrivap  12111  pw2dvdslemn  12703  isnsgrp  13455  ivthinclemdisj  15330  dvply1  15455  lgseisenlem1  15765  lgsquadlem3  15774  structiedg0val  15857  umgr2edg1  16023  umgr2edgneu  16026  pwtrufal  16450  pw1nct  16456  nninfsellemsuc  16466