ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5ibcom Structured version   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  2694  rmob  2823  preqr1g  3507  issod  4026  sotritrieq  4032  nsuceq0g  4100  suctrALT  4103  suc11g  4215  iss  4577  poirr2  4640  xp11m  4682  tz6.12c  5124  fnbrfvb  5135  fvelimab  5150  foeqcnvco  5351  f1eqcocnv  5352  acexmidlemcase  5427  nna0r  5968  nnawordex  6008  ectocld  6079  ecoptocl  6100  ltexnqq  6260  nsmallnqq  6263  nqprloc  6394  0re  6623  0cnALT  6788  bj-peano4  7316
  Copyright terms: Public domain W3C validator