ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylnibr Unicode version

Theorem sylnibr 678
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
StepHypRef Expression
1 sylnibr.1 . 2  |-  ( ph  ->  -.  ps )
2 sylnibr.2 . . 3  |-  ( ch  <->  ps )
32bicomi 132 . 2  |-  ( ps  <->  ch )
41, 3sylnib 677 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
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 615  ax-in2 616
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  rexnalim  2479  nssr  3230  difdif  3275  unssin  3389  inssun  3390  undif3ss  3411  ssdif0im  3502  dcun  3548  prneimg  3789  iundif2ss  3967  nssssr  4240  pofun  4330  frirrg  4368  regexmidlem1  4550  dcdifsnid  6530  unfidisj  6951  fidcenumlemrks  6983  difinfsn  7130  pw1nel3  7261  addnqprlemfl  7589  addnqprlemfu  7590  mulnqprlemfl  7605  mulnqprlemfu  7606  cauappcvgprlemladdru  7686  caucvgprprlemaddq  7738  fzpreddisj  10103  fprodntrivap  11627  pw2dvdslemn  12200  isnsgrp  12884  ivthinclemdisj  14595  lgseisenlem1  14928  pwtrufal  15226  pw1nct  15231  nninfsellemsuc  15240
  Copyright terms: Public domain W3C validator