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  3371  preqr1g  3503  opth1  3939  euotd  3957  reusv3  4133  alxfr  4134  reuhypd  4144  ordsucim  4167  suc11g  4210  nlimsucg  4217  onpsssuc  4222  xpsspw  4368  funcnvuni  4885  fvmptdv2  5176  foco2  5234  fsn  5251  fconst2g  5292  funfvima  5306  isores3  5371  eusvobj2  5413  ovmpt2dv2  5548  ovelrn  5563  f1opw2  5620  suppssfv  5622  suppssov1  5623  nnmordi  5991  nnmord  5992  qsss  6067  eroveu  6099  th3qlem1  6110  addnidpig  6185  enq0tr  6278  prcdnql  6327  prcunqu  6328  genipv  6352  genpelvl  6355  genpelvu  6356  distrlem5prl  6414  distrlem5pru  6415  aptiprlemu  6464  mulid1  6628  ltne  6706  cnegex  6792  creur  7497  creui  7498  cju  7499  nnsub  7538  un0addcl  7792  un0mulcl  7793  zaddcl  7861  qmulz  8108  qre  8110  qnegcl  8121  xrltne  8272  iccid  8337  bj-peano4  8595
  Copyright terms: Public domain W3C validator