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  3843  opth1  4321  euotd  4340  tz7.2  4444  reusv3  4550  alxfr  4551  reuhypd  4561  ordsucim  4591  suc11g  4648  nlimsucg  4657  xpsspw  4830  funcnvuni  5389  fvmptdv2  5723  fsn  5806  fconst2g  5853  funfvima  5870  foco2  5876  isores3  5938  riotaeqimp  5978  eusvobj2  5986  ovmpodv2  6137  ovelrn  6153  f1opw2  6210  suppssfv  6212  suppssov1  6213  nnmordi  6660  nnmord  6661  qsss  6739  eroveu  6771  th3qlem1  6782  mapsncnv  6840  elixpsn  6880  ixpsnf1o  6881  en1bg  6950  pw2f1odclem  6991  mapxpen  7005  en1eqsnbi  7112  updjud  7245  addnidpig  7519  enq0tr  7617  prcdnql  7667  prcunqu  7668  genipv  7692  genpelvl  7695  genpelvu  7696  distrlem5prl  7769  distrlem5pru  7770  aptiprlemu  7823  mulrid  8139  ltne  8227  cnegex  8320  creur  9102  creui  9103  cju  9104  nnsub  9145  un0addcl  9398  un0mulcl  9399  zaddcl  9482  elz2  9514  qmulz  9814  qre  9816  qnegcl  9827  elpqb  9841  xrltne  10005  xlesubadd  10075  iccid  10117  fzsn  10258  fzsuc2  10271  fz1sbc  10288  elfzp12  10291  modqmuladd  10583  bcval5  10980  bcpasc  10983  hashprg  11025  hashfzo  11039  wrdl1s1  11158  cats1un  11248  swrdccat3blem  11266  shftlem  11322  replim  11365  sqrtsq  11550  absle  11595  maxabslemval  11714  negfi  11734  xrmaxiflemval  11756  summodclem2  11888  summodc  11889  zsumdc  11890  fsum3  11893  fsummulc2  11954  fsum00  11968  isumsplit  11997  prodmodclem2  12083  prodmodc  12084  zproddc  12085  fprodseq  12089  prodsnf  12098  fzo0dvdseq  12363  divalgmod  12433  gcdabs1  12505  dvdsgcd  12528  dvdsmulgcd  12541  lcmgcdeq  12600  isprm2lem  12633  dvdsprime  12639  coprm  12661  prmdvdsexpr  12667  rpexp  12670  phibndlem  12733  dfphi2  12737  hashgcdlem  12755  odzdvds  12763  nnoddn2prm  12778  pythagtriplem1  12783  pceulem  12812  pcqmul  12821  pcqcl  12824  pcxnn0cl  12828  pcxcl  12829  pcneg  12843  pcabs  12844  pcgcd1  12846  pcz  12850  pcprmpw2  12851  pcprmpw  12852  dvdsprmpweqle  12855  difsqpwdvds  12856  pcaddlem  12857  pcadd  12858  pcmpt  12861  pockthg  12875  4sqlem2  12907  4sqlem4  12910  mul4sq  12912  mnd1id  13484  0subm  13512  mulgnn0p1  13665  mulgnn0ass  13690  dvreq1  14100  nzrunit  14146  rrgeq0  14223  domneq0  14230  lmodfopnelem2  14283  lss1d  14341  lspsneq0  14384  znidom  14615  znunit  14617  znrrg  14618  istopon  14681  eltg3  14725  tgidm  14742  restbasg  14836  tgrest  14837  tgcn  14876  cnconst  14902  lmss  14914  txbas  14926  txbasval  14935  upxp  14940  blssps  15095  blss  15096  metrest  15174  blssioo  15221  elcncf1di  15247  elply2  15403  plyf  15405  dvdsppwf1o  15657  perfectlem2  15668  perfect  15669  lgsmod  15699  lgsne0  15711  lgsdirnn0  15720  gausslemma2dlem1a  15731  gausslemma2dlem6  15740  lgseisenlem2  15744  lgsquadlem1  15750  lgsquadlem2  15751  2lgslem1b  15762  2sqlem2  15788  mul2sq  15789  2sqlem7  15794  lpvtx  15873  usgredgop  15965  bj-peano4  16276