Theorem sylnibr 677

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 676	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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexnalim  2466  nssr  3215  difdif  3260  unssin  3374  inssun  3375  undif3ss  3396  ssdif0im  3487  dcun  3533  prneimg  3774  iundif2ss  3952  nssssr  4222  pofun  4312  frirrg  4350  regexmidlem1  4532  dcdifsnid  6504  unfidisj  6920  fidcenumlemrks  6951  difinfsn  7098  pw1nel3  7229  addnqprlemfl  7557  addnqprlemfu  7558  mulnqprlemfl  7573  mulnqprlemfu  7574  cauappcvgprlemladdru  7654  caucvgprprlemaddq  7706  fzpreddisj  10070  fprodntrivap  11591  pw2dvdslemn  12164  isnsgrp  12811  ivthinclemdisj  14088  lgseisenlem1  14420  pwtrufal  14717  pw1nct  14722  nninfsellemsuc  14731