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

Theorem syl5ibrcom 146
Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)
Hypotheses
Ref Expression
syl5ibr.1 (φθ)
syl5ibr.2 (χ → (ψθ))
Assertion
Ref Expression
syl5ibrcom (φ → (χψ))

Proof of Theorem syl5ibrcom
StepHypRef Expression
1 syl5ibr.1 . . 3 (φθ)
2 syl5ibr.2 . . 3 (χ → (ψθ))
31, 2syl5ibr 145 . 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  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  biimprcd  149  elsnc2g  3396  preqr1g  3528  opth1  3964  euotd  3982  reusv3  4158  alxfr  4159  reuhypd  4169  ordsucim  4192  suc11g  4235  nlimsucg  4242  onpsssuc  4247  xpsspw  4393  funcnvuni  4911  fvmptdv2  5203  foco2  5261  fsn  5278  fconst2g  5319  funfvima  5333  isores3  5398  eusvobj2  5441  ovmpt2dv2  5576  ovelrn  5591  f1opw2  5648  suppssfv  5650  suppssov1  5651  nnmordi  6025  nnmord  6026  qsss  6101  eroveu  6133  th3qlem1  6144  en1bg  6216  addnidpig  6320  enq0tr  6417  prcdnql  6467  prcunqu  6468  genipv  6492  genpelvl  6495  genpelvu  6496  distrlem5prl  6562  distrlem5pru  6563  aptiprlemu  6612  mulid1  6822  ltne  6900  cnegex  6986  creur  7692  creui  7693  cju  7694  nnsub  7733  un0addcl  7991  un0mulcl  7992  zaddcl  8061  elz2  8088  qmulz  8334  qre  8336  qnegcl  8347  xrltne  8499  iccid  8564  fzsn  8699  fzsuc2  8711  fz1sbc  8728  elfzp12  8731  replim  9087  sqrtsq  9214  bj-peano4  9415
  Copyright terms: Public domain W3C validator