Theorem sylnibr 688

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 687	1 |- ( ph -> -. ch )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  rexnalim  2539  nssr  3308  difdif  3354  unssin  3470  inssun  3471  undif3ss  3492  ssdif0im  3589  dcun  3637  prneimg  3899  iundif2ss  4078  nssssr  4362  pofun  4457  frirrg  4495  regexmidlem1  4680  dcdifsnid  6777  elssdc  7209  unfidisj  7229  fidcenumlemrks  7270  difinfsn  7441  pw1nel3  7591  addnqprlemfl  7927  addnqprlemfu  7928  mulnqprlemfl  7943  mulnqprlemfu  7944  cauappcvgprlemladdru  8024  caucvgprprlemaddq  8076  fzpreddisj  10489  ccatalpha  11397  fprodntrivap  12370  pwbdvdslemn  12963  isnsgrp  13774  ivthinclemdisj  15832  dvply1  15957  lgseisenlem1  16355  lgsquadlem3  16364  structiedg0val  16447  umgr2edg1  16616  umgr2edgneu  16619  trlsegvdegfi  16874  pwtrufal  17193  pw1nct  17199  nninfsellemsuc  17221