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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimprcd  160  elsn2g  3742  preqr1g  3891  opth1  4376  euotd  4395  tz7.2  4499  reusv3  4606  alxfr  4607  reuhypd  4617  ordsucim  4647  suc11g  4704  nlimsucg  4713  xpsspw  4887  funcnvuni  5450  fvmptdv2  5795  fsn  5880  fconst2g  5930  funfvima  5950  foco2  5959  isores3  6021  riotaeqimp  6063  eusvobj2  6071  ovmpodv2  6222  ovelrn  6238  f1opw2  6296  suppssov1  6299  suppssfvg  6503  nnmordi  6789  nnmord  6790  qsss  6868  eroveu  6900  th3qlem1  6911  mapsncnv  6977  elixpsn  7017  ixpsnf1o  7018  en1bg  7087  pw2f1odclem  7134  mapxpen  7148  mapunen  7151  en1eqsnbi  7266  updjud  7422  addnidpig  7703  enq0tr  7801  prcdnql  7851  prcunqu  7852  genipv  7876  genpelvl  7879  genpelvu  7880  distrlem5prl  7953  distrlem5pru  7954  aptiprlemu  8007  mulrid  8323  ltne  8410  cnegex  8504  creur  9289  creui  9290  cju  9291  nnsub  9343  un0addcl  9596  un0mulcl  9597  zaddcl  9684  elz2  9716  qmulz  10023  qre  10025  qnegcl  10036  elpqb  10050  xrltne  10215  xlesubadd  10285  iccid  10327  fzsn  10472  fzsuc2  10486  fz1sbc  10503  elfzp12  10506  modqmuladd  10803  bcval5  11201  bcpasc  11204  hashprg  11249  hashfzo  11263  wrdl1s1  11398  cats1un  11493  swrdccat3blem  11511  shftlem  11581  replim  11624  sqrtsq  11810  absle  11855  maxabslemval  11974  negfi  11994  xrmaxiflemval  12016  summodclem2  12149  summodc  12150  zsumdc  12151  fsum3  12154  fsummulc2  12215  fsum00  12229  isumsplit  12258  prodmodclem2  12344  prodmodc  12345  zproddc  12346  fprodseq  12350  prodsnf  12359  fzo0dvdseq  12624  divalgmod  12694  gcdabs1  12766  dvdsgcd  12789  dvdsmulgcd  12802  lcmgcdeq  12861  isprm2lem  12894  dvdsprime  12900  coprm  12922  prmdvdsexpr  12928  rpexp  12931  phibndlem  12994  dfphi2  12998  hashgcdlem  13016  odzdvds  13024  nnoddn2prm  13039  pythagtriplem1  13044  pceulem  13073  pcqmul  13082  pcqcl  13085  pcxnn0cl  13089  pcxcl  13090  pcneg  13104  pcabs  13105  pcgcd1  13107  pcz  13111  pcprmpw2  13112  pcprmpw  13113  dvdsprmpweqle  13116  difsqpwdvds  13117  pcaddlem  13118  pcadd  13119  pcmpt  13122  pockthg  13136  4sqlem2  13168  4sqlem4  13171  mul4sq  13173  ballotfilemfc0  13232  ballotfilemfcc  13233  mnd1id  13763  0subm  13791  mulgnn0p1  13936  mulgnn0ass  13961  dvreq1  14449  nzrunit  14495  rrgeq0  14573  domneq0  14581  lmodfopnelem2  14662  lss1d  14720  lspsneq0  14763  gsumfsum  14923  znidom  14992  znunit  14994  znrrg  14995  istopon  15114  eltg3  15158  tgidm  15175  restbasg  15269  tgrest  15270  tgcn  15309  cnconst  15335  lmss  15347  txbas  15359  txbasval  15368  upxp  15373  blssps  15528  blss  15529  metrest  15607  blssioo  15654  elcncf1di  15680  elply2  15836  plyf  15838  dvdsppwf1o  16103  perfectlem2  16114  perfect  16115  lgsmod  16145  lgsne0  16157  lgsdirnn0  16166  gausslemma2dlem1a  16177  gausslemma2dlem6  16186  lgseisenlem2  16190  lgsquadlem1  16196  lgsquadlem2  16197  2lgslem1b  16208  2sqlem2  16234  mul2sq  16235  2sqlem7  16240  lpvtx  16320  usgredgop  16414  uhgrspansubgrlem  16517  vtxd0nedgbfi  16540  wlk1walkdom  16600  upgrwlkvtxedg  16605  clwwlkext2edg  16663  clwwlknonccat  16674  bj-peano4  16981