Theorem sylnbi 306

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses

Ref	Expression
sylnbi.1
sylnbi.2

Assertion

Ref	Expression
sylnbi

Proof of Theorem sylnbi

Step	Hyp	Ref	Expression
1		sylnbi.1	. . 3
2	1	notbii 296	. 2
3		sylnbi.2	. 2
4	2, 3	sylbi 195	1

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

This theorem is referenced by:  sylnbir  307  reuun2  3780  opswap  5500  iotanul  5571  riotaund  6293  ndmovcom  6462  suppssov1  6951  suppssfv  6955  brtpos  6983  snnen2o  7726  ranklim  8283  rankuni  8302  cdacomen  8582  ituniiun  8823  hashprb  12462  1mavmul  19050  frgrancvvdeqlem2  25031  frgrawopreglem3  25046  nonbooli  26569  disjunsn  27453  ndmaovcl  32288  ndmaovcom  32290  lindslinindsimp1  33058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185