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

Step	Hyp	Ref	Expression
1		syl5ibr.1	. . 3 |- ( ph -> th )
2		syl5ibr.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	1, 2	syl5ibr 155	. 2 |- ( ch -> ( ph -> ps ) )
4	3	com12 30	1 |- ( ph -> ( ch -> ps ) )

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  3593  preqr1g  3729  opth1  4195  euotd  4213  tz7.2  4313  reusv3  4418  alxfr  4419  reuhypd  4429  ordsucim  4457  suc11g  4514  nlimsucg  4523  xpsspw  4695  funcnvuni  5236  fvmptdv2  5554  fsn  5636  fconst2g  5679  funfvima  5693  foco2  5699  isores3  5760  eusvobj2  5804  ovmpodv2  5948  ovelrn  5963  f1opw2  6020  suppssfv  6022  suppssov1  6023  nnmordi  6456  nnmord  6457  qsss  6532  eroveu  6564  th3qlem1  6575  mapsncnv  6633  elixpsn  6673  ixpsnf1o  6674  en1bg  6738  mapxpen  6786  en1eqsnbi  6886  updjud  7016  addnidpig  7239  enq0tr  7337  prcdnql  7387  prcunqu  7388  genipv  7412  genpelvl  7415  genpelvu  7416  distrlem5prl  7489  distrlem5pru  7490  aptiprlemu  7543  mulid1  7858  ltne  7945  cnegex  8036  creur  8813  creui  8814  cju  8815  nnsub  8855  un0addcl  9106  un0mulcl  9107  zaddcl  9190  elz2  9218  qmulz  9514  qre  9516  qnegcl  9527  elpqb  9540  xrltne  9699  xlesubadd  9769  iccid  9811  fzsn  9950  fzsuc2  9963  fz1sbc  9980  elfzp12  9983  modqmuladd  10247  bcval5  10619  bcpasc  10622  hashprg  10664  hashfzo  10678  shftlem  10698  replim  10741  sqrtsq  10926  absle  10971  maxabslemval  11090  negfi  11109  xrmaxiflemval  11129  summodclem2  11261  summodc  11262  zsumdc  11263  fsum3  11266  fsummulc2  11327  fsum00  11341  isumsplit  11370  prodmodclem2  11456  prodmodc  11457  zproddc  11458  fprodseq  11462  prodsnf  11471  fzo0dvdseq  11730  divalgmod  11799  gcdabs1  11853  dvdsgcd  11876  dvdsmulgcd  11889  lcmgcdeq  11940  isprm2lem  11973  dvdsprime  11979  coprm  11998  prmdvdsexpr  12004  rpexp  12007  phibndlem  12068  dfphi2  12072  hashgcdlem  12090  istopon  12371  eltg3  12417  tgidm  12434  restbasg  12528  tgrest  12529  tgcn  12568  cnconst  12594  lmss  12606  txbas  12618  txbasval  12627  upxp  12632  blssps  12787  blss  12788  metrest  12866  blssioo  12905  elcncf1di  12926  bj-peano4  13490