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  8685  creui  8686  cju  8687  nnsub  8727  un0addcl  8978  un0mulcl  8979  zaddcl  9062  elz2  9090  qmulz  9383  qre  9385  qnegcl  9396  xrltne  9564  xlesubadd  9634  iccid  9676  fzsn  9814  fzsuc2  9827  fz1sbc  9844  elfzp12  9847  modqmuladd  10107  bcval5  10477  bcpasc  10480  hashprg  10522  hashfzo  10536  shftlem  10556  replim  10599  sqrtsq  10784  absle  10829  maxabslemval  10948  negfi  10967  xrmaxiflemval  10987  summodclem2  11119  summodc  11120  zsumdc  11121  fsum3  11124  fsummulc2  11185  fsum00  11199  isumsplit  11228  fzo0dvdseq  11482  divalgmod  11551  gcdabs1  11604  dvdsgcd  11627  dvdsmulgcd  11640  lcmgcdeq  11691  isprm2lem  11724  dvdsprime  11730  coprm  11749  prmdvdsexpr  11755  rpexp  11758  phibndlem  11819  dfphi2  11823  hashgcdlem  11830  istopon  12107  eltg3  12153  tgidm  12170  restbasg  12264  tgrest  12265  tgcn  12304  cnconst  12330  lmss  12342  txbas  12354  txbasval  12363  upxp  12368  blssps  12523  blss  12524  metrest  12602  blssioo  12641  elcncf1di  12662  bj-peano4  13080
  Copyright terms: Public domain W3C validator