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

Theorem syl5ib 147
 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 136 . 2 (𝜒 → (𝜓𝜃))
41, 3syl5 32 1 (𝜒 → (𝜑𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  syl5ibcom  148  syl5ibr  149  sbft  1744  gencl  2603  spsbc  2798  ssnelpss  3317  prexgOLD  3974  prexg  3975  posng  4440  sosng  4441  optocl  4444  relcnvexb  4885  funimass1  5004  dmfex  5107  f1ocnvb  5168  eqfnfv2  5294  elpreima  5314  dff13  5435  f1ocnvfv  5447  f1ocnvfvb  5448  fliftfun  5464  eusvobj2  5526  mpt2xopn0yelv  5885  rntpos  5903  erexb  6162  findcard2  6377  findcard2s  6378  enq0tr  6590  addnqprllem  6683  addnqprulem  6684  distrlem1prl  6738  distrlem1pru  6739  recexprlem1ssl  6789  recexprlem1ssu  6790  elrealeu  6964  addcan  7254  addcan2  7255  neg11  7325  negreb  7339  mulcanapd  7716  receuap  7724  cju  7989  nn1suc  8009  nnaddcl  8010  nndivtr  8031  znegclb  8335  zaddcllempos  8339  zmulcl  8355  zeo  8402  uz11  8591  uzp1  8602  eqreznegel  8646  xneg11  8848  modqadd1  9311  modqmul1  9327  frec2uzltd  9353  bccmpl  9622  cj11  9733  rennim  9829  resqrexlemgt0  9847  dvdsabseq  10159  bj-prexg  10418  strcollnft  10496
 Copyright terms: Public domain W3C validator