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

Theorem syl5ibrcom 156
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 155 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
43com12 30 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biimprcd  159  elsn2g  3528  preqr1g  3663  opth1  4128  euotd  4146  tz7.2  4246  reusv3  4351  alxfr  4352  reuhypd  4362  ordsucim  4386  suc11g  4442  nlimsucg  4451  xpsspw  4621  funcnvuni  5162  fvmptdv2  5478  fsn  5560  fconst2g  5603  funfvima  5617  foco2  5623  isores3  5684  eusvobj2  5728  ovmpodv2  5872  ovelrn  5887  f1opw2  5944  suppssfv  5946  suppssov1  5947  nnmordi  6380  nnmord  6381  qsss  6456  eroveu  6488  th3qlem1  6499  mapsncnv  6557  elixpsn  6597  ixpsnf1o  6598  en1bg  6662  mapxpen  6710  en1eqsnbi  6805  updjud  6935  addnidpig  7112  enq0tr  7210  prcdnql  7260  prcunqu  7261  genipv  7285  genpelvl  7288  genpelvu  7289  distrlem5prl  7362  distrlem5pru  7363  aptiprlemu  7416  mulid1  7731  ltne  7817  cnegex  7908  creur  8681  creui  8682  cju  8683  nnsub  8723  un0addcl  8968  un0mulcl  8969  zaddcl  9052  elz2  9080  qmulz  9371  qre  9373  qnegcl  9384  xrltne  9551  xlesubadd  9621  iccid  9663  fzsn  9801  fzsuc2  9814  fz1sbc  9831  elfzp12  9834  modqmuladd  10094  bcval5  10464  bcpasc  10467  hashprg  10509  hashfzo  10523  shftlem  10543  replim  10586  sqrtsq  10771  absle  10816  maxabslemval  10935  negfi  10954  xrmaxiflemval  10974  summodclem2  11106  summodc  11107  zsumdc  11108  fsum3  11111  fsummulc2  11172  fsum00  11186  isumsplit  11215  fzo0dvdseq  11467  divalgmod  11536  gcdabs1  11589  dvdsgcd  11612  dvdsmulgcd  11625  lcmgcdeq  11676  isprm2lem  11709  dvdsprime  11715  coprm  11734  prmdvdsexpr  11740  rpexp  11743  phibndlem  11803  dfphi2  11807  hashgcdlem  11814  istopon  12091  eltg3  12137  tgidm  12154  restbasg  12248  tgrest  12249  tgcn  12288  cnconst  12314  lmss  12326  txbas  12338  txbasval  12347  upxp  12352  blssps  12507  blss  12508  metrest  12586  blssioo  12625  elcncf1di  12646  bj-peano4  13049
  Copyright terms: Public domain W3C validator