Theorem sylnibr 684

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 683	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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2522  nssr  3288  difdif  3334  unssin  3448  inssun  3449  undif3ss  3470  ssdif0im  3561  dcun  3606  prneimg  3862  iundif2ss  4041  nssssr  4320  pofun  4415  frirrg  4453  regexmidlem1  4637  dcdifsnid  6715  elssdc  7137  unfidisj  7157  fidcenumlemrks  7195  difinfsn  7359  pw1nel3  7509  addnqprlemfl  7839  addnqprlemfu  7840  mulnqprlemfl  7855  mulnqprlemfu  7856  cauappcvgprlemladdru  7936  caucvgprprlemaddq  7988  fzpreddisj  10368  ccatalpha  11256  fprodntrivap  12225  pw2dvdslemn  12817  isnsgrp  13569  ivthinclemdisj  15451  dvply1  15576  lgseisenlem1  15889  lgsquadlem3  15898  structiedg0val  15981  umgr2edg1  16150  umgr2edgneu  16153  trlsegvdegfi  16408  pwtrufal  16719  pw1nct  16725  nninfsellemsuc  16738