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  3666  preqr1g  3807  opth1  4280  euotd  4299  tz7.2  4401  reusv3  4507  alxfr  4508  reuhypd  4518  ordsucim  4548  suc11g  4605  nlimsucg  4614  xpsspw  4787  funcnvuni  5343  fvmptdv2  5669  fsn  5752  fconst2g  5799  funfvima  5816  foco2  5822  isores3  5884  eusvobj2  5930  ovmpodv2  6079  ovelrn  6095  f1opw2  6152  suppssfv  6154  suppssov1  6155  nnmordi  6602  nnmord  6603  qsss  6681  eroveu  6713  th3qlem1  6724  mapsncnv  6782  elixpsn  6822  ixpsnf1o  6823  en1bg  6892  pw2f1odclem  6931  mapxpen  6945  en1eqsnbi  7051  updjud  7184  addnidpig  7449  enq0tr  7547  prcdnql  7597  prcunqu  7598  genipv  7622  genpelvl  7625  genpelvu  7626  distrlem5prl  7699  distrlem5pru  7700  aptiprlemu  7753  mulrid  8069  ltne  8157  cnegex  8250  creur  9032  creui  9033  cju  9034  nnsub  9075  un0addcl  9328  un0mulcl  9329  zaddcl  9412  elz2  9444  qmulz  9744  qre  9746  qnegcl  9757  elpqb  9771  xrltne  9935  xlesubadd  10005  iccid  10047  fzsn  10188  fzsuc2  10201  fz1sbc  10218  elfzp12  10221  modqmuladd  10511  bcval5  10908  bcpasc  10911  hashprg  10953  hashfzo  10967  wrdl1s1  11084  shftlem  11127  replim  11170  sqrtsq  11355  absle  11400  maxabslemval  11519  negfi  11539  xrmaxiflemval  11561  summodclem2  11693  summodc  11694  zsumdc  11695  fsum3  11698  fsummulc2  11759  fsum00  11773  isumsplit  11802  prodmodclem2  11888  prodmodc  11889  zproddc  11890  fprodseq  11894  prodsnf  11903  fzo0dvdseq  12168  divalgmod  12238  gcdabs1  12310  dvdsgcd  12333  dvdsmulgcd  12346  lcmgcdeq  12405  isprm2lem  12438  dvdsprime  12444  coprm  12466  prmdvdsexpr  12472  rpexp  12475  phibndlem  12538  dfphi2  12542  hashgcdlem  12560  odzdvds  12568  nnoddn2prm  12583  pythagtriplem1  12588  pceulem  12617  pcqmul  12626  pcqcl  12629  pcxnn0cl  12633  pcxcl  12634  pcneg  12648  pcabs  12649  pcgcd1  12651  pcz  12655  pcprmpw2  12656  pcprmpw  12657  dvdsprmpweqle  12660  difsqpwdvds  12661  pcaddlem  12662  pcadd  12663  pcmpt  12666  pockthg  12680  4sqlem2  12712  4sqlem4  12715  mul4sq  12717  mnd1id  13288  0subm  13316  mulgnn0p1  13469  mulgnn0ass  13494  dvreq1  13904  nzrunit  13950  rrgeq0  14027  domneq0  14034  lmodfopnelem2  14087  lss1d  14145  lspsneq0  14188  znidom  14419  znunit  14421  znrrg  14422  istopon  14485  eltg3  14529  tgidm  14546  restbasg  14640  tgrest  14641  tgcn  14680  cnconst  14706  lmss  14718  txbas  14730  txbasval  14739  upxp  14744  blssps  14899  blss  14900  metrest  14978  blssioo  15025  elcncf1di  15051  elply2  15207  plyf  15209  dvdsppwf1o  15461  perfectlem2  15472  perfect  15473  lgsmod  15503  lgsne0  15515  lgsdirnn0  15524  gausslemma2dlem1a  15535  gausslemma2dlem6  15544  lgseisenlem2  15548  lgsquadlem1  15554  lgsquadlem2  15555  2lgslem1b  15566  2sqlem2  15592  mul2sq  15593  2sqlem7  15598  bj-peano4  15891