Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5ibcom GIF 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  2721  rmob  2850  preqr1g  3537  issod  4056  sotritrieq  4062  nsuceq0g  4155  suctr  4158  nordeq  4268  suc11g  4281  iss  4654  poirr2  4717  xp11m  4759  tz6.12c  5203  fnbrfvb  5214  fvelimab  5229  foeqcnvco  5430  f1eqcocnv  5431  acexmidlemcase  5507  nna0r  6057  nnawordex  6101  ectocld  6172  ecoptocl  6193  eqeng  6246  fopwdom  6310  ordiso  6358  ltexnqq  6506  nsmallnqq  6510  nqprloc  6643  aptiprleml  6737  0re  7027  lttri3  7098  0cnALT  7201  reapti  7570  recnz  8333  zneo  8339  uzn0  8488  flqidz  9128  ceilqidz  9158  frec2uzrand  9191  frecuzrdgfn  9198  iseqid  9247  bj-peano4  10080
 Copyright terms: Public domain W3C validator