Theorem sylnibr 679

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 678	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2497  nssr  3261  difdif  3306  unssin  3420  inssun  3421  undif3ss  3442  ssdif0im  3533  dcun  3578  prneimg  3828  iundif2ss  4007  nssssr  4284  pofun  4377  frirrg  4415  regexmidlem1  4599  dcdifsnid  6613  unfidisj  7045  fidcenumlemrks  7081  difinfsn  7228  pw1nel3  7377  addnqprlemfl  7707  addnqprlemfu  7708  mulnqprlemfl  7723  mulnqprlemfu  7724  cauappcvgprlemladdru  7804  caucvgprprlemaddq  7856  fzpreddisj  10228  fprodntrivap  12010  pw2dvdslemn  12602  isnsgrp  13353  ivthinclemdisj  15227  dvply1  15352  lgseisenlem1  15662  lgsquadlem3  15671  structiedg0val  15754  pwtrufal  16136  pw1nct  16142  nninfsellemsuc  16151