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

Theorem syl5ibrcom 150
Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)
Hypotheses
Ref Expression
syl5ibr.1  |-  ( ph  ->  th )
syl5ibr.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ibrcom  |-  ( ph  ->  ( ch  ->  ps ) )

Proof of Theorem syl5ibrcom
StepHypRef Expression
1 syl5ibr.1 . . 3  |-  ( ph  ->  th )
2 syl5ibr.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
31, 2syl5ibr 149 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
43com12 30 1  |-  ( ph  ->  ( ch  ->  ps ) )
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  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  biimprcd  153  elsn2g  3432  preqr1g  3565  opth1  4001  euotd  4019  tz7.2  4119  reusv3  4220  alxfr  4221  reuhypd  4231  ordsucim  4254  suc11g  4309  nlimsucg  4318  onpsssuc  4323  xpsspw  4478  funcnvuni  4996  fvmptdv2  5288  foco2  5346  fsn  5363  fconst2g  5404  funfvima  5418  isores3  5483  eusvobj2  5526  ovmpt2dv2  5662  ovelrn  5677  f1opw2  5734  suppssfv  5736  suppssov1  5737  nnmordi  6120  nnmord  6121  qsss  6196  eroveu  6228  th3qlem1  6239  en1bg  6311  addnidpig  6492  enq0tr  6590  prcdnql  6640  prcunqu  6641  genipv  6665  genpelvl  6668  genpelvu  6669  distrlem5prl  6742  distrlem5pru  6743  aptiprlemu  6796  mulid1  7082  ltne  7162  cnegex  7252  creur  7987  creui  7988  cju  7989  nnsub  8028  un0addcl  8272  un0mulcl  8273  zaddcl  8342  elz2  8370  qmulz  8655  qre  8657  qnegcl  8668  xrltne  8830  iccid  8895  fzsn  9031  fzsuc2  9043  fz1sbc  9060  elfzp12  9063  modqmuladd  9316  iseqid3  9409  ibcval5  9631  bcpasc  9634  shftlem  9645  replim  9687  sqrtsq  9871  absle  9916  fzo0dvdseq  10169  divalgmod  10239  bj-peano4  10467
  Copyright terms: Public domain W3C validator