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  3727  preqr1g  3875  opth1  4357  euotd  4376  tz7.2  4480  reusv3  4586  alxfr  4587  reuhypd  4597  ordsucim  4627  suc11g  4684  nlimsucg  4693  xpsspw  4867  funcnvuni  5430  fvmptdv2  5772  fsn  5854  fconst2g  5904  funfvima  5923  foco2  5932  isores3  5994  riotaeqimp  6036  eusvobj2  6044  ovmpodv2  6195  ovelrn  6211  f1opw2  6269  suppssov1  6272  suppssfvg  6476  nnmordi  6762  nnmord  6763  qsss  6841  eroveu  6873  th3qlem1  6884  mapsncnv  6943  elixpsn  6983  ixpsnf1o  6984  en1bg  7053  pw2f1odclem  7100  mapxpen  7114  mapunen  7117  en1eqsnbi  7232  updjud  7386  addnidpig  7667  enq0tr  7765  prcdnql  7815  prcunqu  7816  genipv  7840  genpelvl  7843  genpelvu  7844  distrlem5prl  7917  distrlem5pru  7918  aptiprlemu  7971  mulrid  8287  ltne  8374  cnegex  8467  creur  9250  creui  9251  cju  9252  nnsub  9293  un0addcl  9546  un0mulcl  9547  zaddcl  9634  elz2  9666  qmulz  9973  qre  9975  qnegcl  9986  elpqb  10000  xrltne  10165  xlesubadd  10235  iccid  10277  fzsn  10421  fzsuc2  10435  fz1sbc  10452  elfzp12  10455  modqmuladd  10752  bcval5  11150  bcpasc  11153  hashprg  11198  hashfzo  11212  wrdl1s1  11343  cats1un  11438  swrdccat3blem  11456  shftlem  11526  replim  11569  sqrtsq  11754  absle  11799  maxabslemval  11918  negfi  11938  xrmaxiflemval  11960  summodclem2  12093  summodc  12094  zsumdc  12095  fsum3  12098  fsummulc2  12159  fsum00  12173  isumsplit  12202  prodmodclem2  12288  prodmodc  12289  zproddc  12290  fprodseq  12294  prodsnf  12303  fzo0dvdseq  12568  divalgmod  12638  gcdabs1  12710  dvdsgcd  12733  dvdsmulgcd  12746  lcmgcdeq  12805  isprm2lem  12838  dvdsprime  12844  coprm  12866  prmdvdsexpr  12872  rpexp  12875  phibndlem  12938  dfphi2  12942  hashgcdlem  12960  odzdvds  12968  nnoddn2prm  12983  pythagtriplem1  12988  pceulem  13017  pcqmul  13026  pcqcl  13029  pcxnn0cl  13033  pcxcl  13034  pcneg  13048  pcabs  13049  pcgcd1  13051  pcz  13055  pcprmpw2  13056  pcprmpw  13057  dvdsprmpweqle  13060  difsqpwdvds  13061  pcaddlem  13062  pcadd  13063  pcmpt  13066  pockthg  13080  4sqlem2  13112  4sqlem4  13115  mul4sq  13117  ballotfilemfc0  13176  ballotfilemfcc  13177  mnd1id  13711  0subm  13739  mulgnn0p1  13886  mulgnn0ass  13911  dvreq1  14387  nzrunit  14433  rrgeq0  14511  domneq0  14519  lmodfopnelem2  14599  lss1d  14657  lspsneq0  14700  znidom  14931  znunit  14933  znrrg  14934  istopon  15004  eltg3  15048  tgidm  15065  restbasg  15159  tgrest  15160  tgcn  15199  cnconst  15225  lmss  15237  txbas  15249  txbasval  15258  upxp  15263  blssps  15418  blss  15419  metrest  15497  blssioo  15544  elcncf1di  15570  elply2  15726  plyf  15728  dvdsppwf1o  15983  perfectlem2  15994  perfect  15995  lgsmod  16025  lgsne0  16037  lgsdirnn0  16046  gausslemma2dlem1a  16057  gausslemma2dlem6  16066  lgseisenlem2  16070  lgsquadlem1  16076  lgsquadlem2  16077  2lgslem1b  16088  2sqlem2  16114  mul2sq  16115  2sqlem7  16120  lpvtx  16200  usgredgop  16294  uhgrspansubgrlem  16397  vtxd0nedgbfi  16420  wlk1walkdom  16480  upgrwlkvtxedg  16485  clwwlkext2edg  16543  clwwlknonccat  16554  bj-peano4  16851