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

Theorem syl5ibcom 144
Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
Hypotheses
Ref Expression
syl5ib.1
syl5ib.2
Assertion
Ref Expression
syl5ibcom

Proof of Theorem syl5ibcom
StepHypRef Expression
1 syl5ib.1 . . 3
2 syl5ib.2 . . 3
31, 2syl5ib 143 . 2
43com12 27 1
Colors of variables: wff set class
Syntax hints:   wi 4   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  biimpcd  148  mob2  2715  rmob  2844  preqr1g  3528  issod  4047  sotritrieq  4053  nsuceq0g  4121  suctr  4124  suc11g  4235  iss  4597  poirr2  4660  xp11m  4702  tz6.12c  5146  fnbrfvb  5157  fvelimab  5172  foeqcnvco  5373  f1eqcocnv  5374  acexmidlemcase  5450  nna0r  5996  nnawordex  6037  ectocld  6108  ecoptocl  6129  eqeng  6182  fopwdom  6246  ltexnqq  6391  nsmallnqq  6395  nqprloc  6528  aptiprleml  6611  0re  6825  lttri3  6895  0cnALT  6998  reapti  7363  recnz  8109  zneo  8115  uzn0  8264  frec2uzrand  8872  frecuzrdgfn  8879  bj-peano4  9415
  Copyright terms: Public domain W3C validator