ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5ibrcom Structured version   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  6416  prcdnql  6466  prcunqu  6467  genipv  6491  genpelvl  6494  genpelvu  6495  distrlem5prl  6561  distrlem5pru  6562  aptiprlemu  6611  mulid1  6802  ltne  6880  cnegex  6966  creur  7672  creui  7673  cju  7674  nnsub  7713  un0addcl  7971  un0mulcl  7972  zaddcl  8041  elz2  8068  qmulz  8314  qre  8316  qnegcl  8327  xrltne  8479  iccid  8544  fzsn  8679  fzsuc2  8691  fz1sbc  8708  elfzp12  8711  replim  9067  sqrtsq  9194  bj-peano4  9389
  Copyright terms: Public domain W3C validator