ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5ib 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  1728  gencl  2586  spsbc  2775  eqsbc3r  2819  ssnelpss  3289  prexgOLD  3946  prexg  3947  posng  4412  sosng  4413  optocl  4416  relcnvexb  4857  funimass1  4976  dmfex  5079  f1ocnvb  5140  eqfnfv2  5266  elpreima  5286  dff13  5407  f1ocnvfv  5419  f1ocnvfvb  5420  fliftfun  5436  eusvobj2  5498  mpt2xopn0yelv  5854  rntpos  5872  erexb  6131  findcard2  6346  findcard2s  6347  enq0tr  6532  addnqprllem  6625  addnqprulem  6626  distrlem1prl  6680  distrlem1pru  6681  recexprlem1ssl  6731  recexprlem1ssu  6732  elrealeu  6906  addcan  7191  addcan2  7192  neg11  7262  negreb  7276  mulcanapd  7642  receuap  7650  cju  7913  nn1suc  7933  nnaddcl  7934  nndivtr  7955  znegclb  8278  zaddcllempos  8282  zmulcl  8297  zeo  8343  uz11  8495  uzp1  8506  eqreznegel  8549  xneg11  8747  frec2uzltd  9189  cj11  9505  rennim  9600  resqrexlemgt0  9618  bj-prexg  10031  strcollnft  10109
  Copyright terms: Public domain W3C validator