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

Theorem sylnibr 667
 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
sylnibr.2
Assertion
Ref Expression
sylnibr

Proof of Theorem sylnibr
StepHypRef Expression
1 sylnibr.1 . 2
2 sylnibr.2 . . 3
32bicomi 131 . 2
41, 3sylnib 666 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  rexnalim  2428  nssr  3162  difdif  3206  unssin  3320  inssun  3321  undif3ss  3342  ssdif0im  3432  dcun  3478  prneimg  3709  iundif2ss  3886  nssssr  4152  pofun  4242  frirrg  4280  regexmidlem1  4456  dcdifsnid  6408  unfidisj  6818  fidcenumlemrks  6849  difinfsn  6993  addnqprlemfl  7392  addnqprlemfu  7393  mulnqprlemfl  7408  mulnqprlemfu  7409  cauappcvgprlemladdru  7489  caucvgprprlemaddq  7541  fzpreddisj  9883  pw2dvdslemn  11880  ivthinclemdisj  12827  pwtrufal  13366  pw1nct  13372  nninfsellemsuc  13384
 Copyright terms: Public domain W3C validator