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  2533  nssr  3302  difdif  3348  unssin  3464  inssun  3465  undif3ss  3486  ssdif0im  3577  dcun  3623  prneimg  3883  iundif2ss  4062  nssssr  4343  pofun  4438  frirrg  4476  regexmidlem1  4660  dcdifsnid  6750  elssdc  7175  unfidisj  7195  fidcenumlemrks  7236  difinfsn  7404  pw1nel3  7554  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemfl  7906  mulnqprlemfu  7907  cauappcvgprlemladdru  7987  caucvgprprlemaddq  8039  fzpreddisj  10427  ccatalpha  11326  fprodntrivap  12295  pw2dvdslemn  12887  isnsgrp  13669  ivthinclemdisj  15631  dvply1  15756  lgseisenlem1  16069  lgsquadlem3  16078  structiedg0val  16161  umgr2edg1  16330  umgr2edgneu  16333  trlsegvdegfi  16588  pwtrufal  16897  pw1nct  16903  nninfsellemsuc  16916