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  2495  nssr  3253  difdif  3298  unssin  3412  inssun  3413  undif3ss  3434  ssdif0im  3525  dcun  3570  prneimg  3815  iundif2ss  3993  nssssr  4267  pofun  4360  frirrg  4398  regexmidlem1  4582  dcdifsnid  6592  unfidisj  7021  fidcenumlemrks  7057  difinfsn  7204  pw1nel3  7345  addnqprlemfl  7674  addnqprlemfu  7675  mulnqprlemfl  7690  mulnqprlemfu  7691  cauappcvgprlemladdru  7771  caucvgprprlemaddq  7823  fzpreddisj  10195  fprodntrivap  11928  pw2dvdslemn  12520  isnsgrp  13271  ivthinclemdisj  15145  dvply1  15270  lgseisenlem1  15580  lgsquadlem3  15589  structiedg0val  15670  pwtrufal  15971  pw1nct  15977  nninfsellemsuc  15986