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  4364  pofun  4459  frirrg  4497  regexmidlem1  4682  dcdifsnid  6781  elssdc  7213  unfidisj  7233  fidcenumlemrks  7275  difinfsn  7446  pw1nel3  7596  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemfl  7948  mulnqprlemfu  7949  cauappcvgprlemladdru  8029  caucvgprprlemaddq  8081  fzpreddisj  10495  ccatalpha  11403  fprodntrivap  12376  pwbdvdslemn  12969  isnsgrp  13780  gsummptfidmsplit  14254  ivthinclemdisj  15866  dvply1  15991  lgseisenlem1  16394  lgsquadlem3  16403  structiedg0val  16486  umgr2edg1  16655  umgr2edgneu  16658  trlsegvdegfi  16913  pwtrufal  17232  pw1nct  17238  nninfsellemsuc  17261