Theorem sylnibr 672

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 131	. 2 |- ( ps <-> ch )
4	1, 3	sylnib 671	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  rexnalim  2459  nssr  3207  difdif  3252  unssin  3366  inssun  3367  undif3ss  3388  ssdif0im  3479  dcun  3525  prneimg  3761  iundif2ss  3938  nssssr  4207  pofun  4297  frirrg  4335  regexmidlem1  4517  dcdifsnid  6483  unfidisj  6899  fidcenumlemrks  6930  difinfsn  7077  pw1nel3  7208  addnqprlemfl  7521  addnqprlemfu  7522  mulnqprlemfl  7537  mulnqprlemfu  7538  cauappcvgprlemladdru  7618  caucvgprprlemaddq  7670  fzpreddisj  10027  fprodntrivap  11547  pw2dvdslemn  12119  isnsgrp  12647  ivthinclemdisj  13412  pwtrufal  14030  pw1nct  14036  nninfsellemsuc  14045