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

Theorem syl5ibrcom 146
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 145 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
43com12 27 1  |-  ( ph  ->  ( ch  ->  ps ) )
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  elsn2g  3401  preqr1g  3534  opth1  3970  euotd  3988  tz7.2  4085  reusv3  4179  alxfr  4180  reuhypd  4190  ordsucim  4213  suc11g  4266  nlimsucg  4275  onpsssuc  4280  xpsspw  4428  funcnvuni  4946  fvmptdv2  5238  foco2  5296  fsn  5313  fconst2g  5354  funfvima  5368  isores3  5433  eusvobj2  5476  ovmpt2dv2  5612  ovelrn  5627  f1opw2  5684  suppssfv  5686  suppssov1  5687  nnmordi  6067  nnmord  6068  qsss  6143  eroveu  6175  th3qlem1  6186  en1bg  6258  addnidpig  6406  enq0tr  6504  prcdnql  6554  prcunqu  6555  genipv  6579  genpelvl  6582  genpelvu  6583  distrlem5prl  6656  distrlem5pru  6657  aptiprlemu  6710  mulid1  6996  ltne  7074  cnegex  7160  creur  7878  creui  7879  cju  7880  nnsub  7919  un0addcl  8178  un0mulcl  8179  zaddcl  8248  elz2  8275  qmulz  8521  qre  8523  qnegcl  8534  xrltne  8687  iccid  8752  fzsn  8887  fzsuc2  8899  fz1sbc  8916  elfzp12  8919  iseqid3  9114  shftlem  9286  replim  9328  sqrtsq  9511  absle  9554  bj-peano4  9944
  Copyright terms: Public domain W3C validator