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

Theorem syl5ib 143
Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5ib.1 (φψ)
syl5ib.2 (χ → (ψθ))
Assertion
Ref Expression
syl5ib (χ → (φθ))

Proof of Theorem syl5ib
StepHypRef Expression
1 syl5ib.1 . 2 (φψ)
2 syl5ib.2 . . 3 (χ → (ψθ))
32biimpd 132 . 2 (χ → (ψθ))
41, 3syl5 28 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:  syl5ibcom  144  syl5ibr  145  sbft  1725  gencl  2580  spsbc  2769  eqsbc3r  2813  ssnelpss  3283  prexgOLD  3937  prexg  3938  posng  4355  sosng  4356  optocl  4359  relcnvexb  4800  funimass1  4919  dmfex  5022  f1ocnvb  5083  eqfnfv2  5209  elpreima  5229  dff13  5350  f1ocnvfv  5362  f1ocnvfvb  5363  fliftfun  5379  eusvobj2  5441  mpt2xopn0yelv  5795  rntpos  5813  erexb  6067  enq0tr  6416  addnqprllem  6509  addnqprulem  6510  distrlem1prl  6557  distrlem1pru  6558  recexprlem1ssl  6604  recexprlem1ssu  6605  addcan  6968  addcan2  6969  neg11  7038  negreb  7052  mulcanapd  7404  receuap  7412  cju  7674  nn1suc  7694  nnaddcl  7695  nndivtr  7716  znegclb  8034  zaddcllempos  8038  zmulcl  8053  zeo  8099  uz11  8251  uzp1  8262  eqreznegel  8305  xneg11  8497  frec2uzltd  8850  cj11  9113  rennim  9191  bj-prexg  9342  strcollnft  9414
  Copyright terms: Public domain W3C validator