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  3553  preqr1g  3688  opth1  4153  euotd  4171  tz7.2  4271  reusv3  4376  alxfr  4377  reuhypd  4387  ordsucim  4411  suc11g  4467  nlimsucg  4476  xpsspw  4646  funcnvuni  5187  fvmptdv2  5503  fsn  5585  fconst2g  5628  funfvima  5642  foco2  5648  isores3  5709  eusvobj2  5753  ovmpodv2  5897  ovelrn  5912  f1opw2  5969  suppssfv  5971  suppssov1  5972  nnmordi  6405  nnmord  6406  qsss  6481  eroveu  6513  th3qlem1  6524  mapsncnv  6582  elixpsn  6622  ixpsnf1o  6623  en1bg  6687  mapxpen  6735  en1eqsnbi  6830  updjud  6960  addnidpig  7137  enq0tr  7235  prcdnql  7285  prcunqu  7286  genipv  7310  genpelvl  7313  genpelvu  7314  distrlem5prl  7387  distrlem5pru  7388  aptiprlemu  7441  mulid1  7756  ltne  7842  cnegex  7933  creur  8710  creui  8711  cju  8712  nnsub  8752  un0addcl  9003  un0mulcl  9004  zaddcl  9087  elz2  9115  qmulz  9408  qre  9410  qnegcl  9421  xrltne  9589  xlesubadd  9659  iccid  9701  fzsn  9839  fzsuc2  9852  fz1sbc  9869  elfzp12  9872  modqmuladd  10132  bcval5  10502  bcpasc  10505  hashprg  10547  hashfzo  10561  shftlem  10581  replim  10624  sqrtsq  10809  absle  10854  maxabslemval  10973  negfi  10992  xrmaxiflemval  11012  summodclem2  11144  summodc  11145  zsumdc  11146  fsum3  11149  fsummulc2  11210  fsum00  11224  isumsplit  11253  fzo0dvdseq  11544  divalgmod  11613  gcdabs1  11666  dvdsgcd  11689  dvdsmulgcd  11702  lcmgcdeq  11753  isprm2lem  11786  dvdsprime  11792  coprm  11811  prmdvdsexpr  11817  rpexp  11820  phibndlem  11881  dfphi2  11885  hashgcdlem  11892  istopon  12169  eltg3  12215  tgidm  12232  restbasg  12326  tgrest  12327  tgcn  12366  cnconst  12392  lmss  12404  txbas  12416  txbasval  12425  upxp  12430  blssps  12585  blss  12586  metrest  12664  blssioo  12703  elcncf1di  12724  bj-peano4  13142