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  6530  addnqprllem  6623  addnqprulem  6624  distrlem1prl  6678  distrlem1pru  6679  recexprlem1ssl  6729  recexprlem1ssu  6730  elrealeu  6904  addcan  7189  addcan2  7190  neg11  7260  negreb  7274  mulcanapd  7640  receuap  7648  cju  7911  nn1suc  7931  nnaddcl  7932  nndivtr  7953  znegclb  8276  zaddcllempos  8280  zmulcl  8295  zeo  8341  uz11  8493  uzp1  8504  eqreznegel  8547  xneg11  8745  frec2uzltd  9163  cj11  9479  rennim  9574  resqrexlemgt0  9592  bj-prexg  10005  strcollnft  10083
  Copyright terms: Public domain W3C validator