Theorem syl5ibrcom 157

Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)

Hypotheses

Ref	Expression
imbitrrid.1	|- ( ph -> th )
imbitrrid.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5ibrcom	|- ( ph -> ( ch -> ps ) )

Proof of Theorem syl5ibrcom

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

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimprcd  160  elsn2g  3699  preqr1g  3844  opth1  4322  euotd  4341  tz7.2  4445  reusv3  4551  alxfr  4552  reuhypd  4562  ordsucim  4592  suc11g  4649  nlimsucg  4658  xpsspw  4831  funcnvuni  5390  fvmptdv2  5726  fsn  5809  fconst2g  5858  funfvima  5875  foco2  5883  isores3  5945  riotaeqimp  5985  eusvobj2  5993  ovmpodv2  6144  ovelrn  6160  f1opw2  6218  suppssfv  6220  suppssov1  6221  nnmordi  6670  nnmord  6671  qsss  6749  eroveu  6781  th3qlem1  6792  mapsncnv  6850  elixpsn  6890  ixpsnf1o  6891  en1bg  6960  pw2f1odclem  7003  mapxpen  7017  en1eqsnbi  7127  updjud  7260  addnidpig  7534  enq0tr  7632  prcdnql  7682  prcunqu  7683  genipv  7707  genpelvl  7710  genpelvu  7711  distrlem5prl  7784  distrlem5pru  7785  aptiprlemu  7838  mulrid  8154  ltne  8242  cnegex  8335  creur  9117  creui  9118  cju  9119  nnsub  9160  un0addcl  9413  un0mulcl  9414  zaddcl  9497  elz2  9529  qmulz  9830  qre  9832  qnegcl  9843  elpqb  9857  xrltne  10021  xlesubadd  10091  iccid  10133  fzsn  10274  fzsuc2  10287  fz1sbc  10304  elfzp12  10307  modqmuladd  10600  bcval5  10997  bcpasc  11000  hashprg  11043  hashfzo  11057  wrdl1s1  11178  cats1un  11268  swrdccat3blem  11286  shftlem  11342  replim  11385  sqrtsq  11570  absle  11615  maxabslemval  11734  negfi  11754  xrmaxiflemval  11776  summodclem2  11908  summodc  11909  zsumdc  11910  fsum3  11913  fsummulc2  11974  fsum00  11988  isumsplit  12017  prodmodclem2  12103  prodmodc  12104  zproddc  12105  fprodseq  12109  prodsnf  12118  fzo0dvdseq  12383  divalgmod  12453  gcdabs1  12525  dvdsgcd  12548  dvdsmulgcd  12561  lcmgcdeq  12620  isprm2lem  12653  dvdsprime  12659  coprm  12681  prmdvdsexpr  12687  rpexp  12690  phibndlem  12753  dfphi2  12757  hashgcdlem  12775  odzdvds  12783  nnoddn2prm  12798  pythagtriplem1  12803  pceulem  12832  pcqmul  12841  pcqcl  12844  pcxnn0cl  12848  pcxcl  12849  pcneg  12863  pcabs  12864  pcgcd1  12866  pcz  12870  pcprmpw2  12871  pcprmpw  12872  dvdsprmpweqle  12875  difsqpwdvds  12876  pcaddlem  12877  pcadd  12878  pcmpt  12881  pockthg  12895  4sqlem2  12927  4sqlem4  12930  mul4sq  12932  mnd1id  13504  0subm  13532  mulgnn0p1  13685  mulgnn0ass  13710  dvreq1  14121  nzrunit  14167  rrgeq0  14244  domneq0  14251  lmodfopnelem2  14304  lss1d  14362  lspsneq0  14405  znidom  14636  znunit  14638  znrrg  14639  istopon  14702  eltg3  14746  tgidm  14763  restbasg  14857  tgrest  14858  tgcn  14897  cnconst  14923  lmss  14935  txbas  14947  txbasval  14956  upxp  14961  blssps  15116  blss  15117  metrest  15195  blssioo  15242  elcncf1di  15268  elply2  15424  plyf  15426  dvdsppwf1o  15678  perfectlem2  15689  perfect  15690  lgsmod  15720  lgsne0  15732  lgsdirnn0  15741  gausslemma2dlem1a  15752  gausslemma2dlem6  15761  lgseisenlem2  15765  lgsquadlem1  15771  lgsquadlem2  15772  2lgslem1b  15783  2sqlem2  15809  mul2sq  15810  2sqlem7  15815  lpvtx  15894  usgredgop  15986  wlk1walkdom  16100  upgrwlkvtxedg  16105  bj-peano4  16373