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

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
StepHypRef Expression
1 sylnibr.1 . 2  |-  ( ph  ->  -.  ps )
2 sylnibr.2 . . 3  |-  ( ch  <->  ps )
32bicomi 132 . 2  |-  ( ps  <->  ch )
41, 3sylnib 676 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 614  ax-in2 615
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  rexnalim  2466  nssr  3216  difdif  3261  unssin  3375  inssun  3376  undif3ss  3397  ssdif0im  3488  dcun  3534  prneimg  3775  iundif2ss  3953  nssssr  4223  pofun  4313  frirrg  4351  regexmidlem1  4533  dcdifsnid  6505  unfidisj  6921  fidcenumlemrks  6952  difinfsn  7099  pw1nel3  7230  addnqprlemfl  7558  addnqprlemfu  7559  mulnqprlemfl  7574  mulnqprlemfu  7575  cauappcvgprlemladdru  7655  caucvgprprlemaddq  7707  fzpreddisj  10071  fprodntrivap  11592  pw2dvdslemn  12165  isnsgrp  12812  ivthinclemdisj  14121  lgseisenlem1  14453  pwtrufal  14750  pw1nct  14755  nninfsellemsuc  14764
  Copyright terms: Public domain W3C validator