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  3652  preqr1g  3793  opth1  4266  euotd  4284  tz7.2  4386  reusv3  4492  alxfr  4493  reuhypd  4503  ordsucim  4533  suc11g  4590  nlimsucg  4599  xpsspw  4772  funcnvuni  5324  fvmptdv2  5648  fsn  5731  fconst2g  5774  funfvima  5791  foco2  5797  isores3  5859  eusvobj2  5905  ovmpodv2  6053  ovelrn  6069  f1opw2  6126  suppssfv  6128  suppssov1  6129  nnmordi  6571  nnmord  6572  qsss  6650  eroveu  6682  th3qlem1  6693  mapsncnv  6751  elixpsn  6791  ixpsnf1o  6792  en1bg  6856  pw2f1odclem  6892  mapxpen  6906  en1eqsnbi  7010  updjud  7143  addnidpig  7398  enq0tr  7496  prcdnql  7546  prcunqu  7547  genipv  7571  genpelvl  7574  genpelvu  7575  distrlem5prl  7648  distrlem5pru  7649  aptiprlemu  7702  mulrid  8018  ltne  8106  cnegex  8199  creur  8980  creui  8981  cju  8982  nnsub  9023  un0addcl  9276  un0mulcl  9277  zaddcl  9360  elz2  9391  qmulz  9691  qre  9693  qnegcl  9704  elpqb  9718  xrltne  9882  xlesubadd  9952  iccid  9994  fzsn  10135  fzsuc2  10148  fz1sbc  10165  elfzp12  10168  modqmuladd  10440  bcval5  10837  bcpasc  10840  hashprg  10882  hashfzo  10896  shftlem  10963  replim  11006  sqrtsq  11191  absle  11236  maxabslemval  11355  negfi  11374  xrmaxiflemval  11396  summodclem2  11528  summodc  11529  zsumdc  11530  fsum3  11533  fsummulc2  11594  fsum00  11608  isumsplit  11637  prodmodclem2  11723  prodmodc  11724  zproddc  11725  fprodseq  11729  prodsnf  11738  fzo0dvdseq  12002  divalgmod  12071  gcdabs1  12129  dvdsgcd  12152  dvdsmulgcd  12165  lcmgcdeq  12224  isprm2lem  12257  dvdsprime  12263  coprm  12285  prmdvdsexpr  12291  rpexp  12294  phibndlem  12357  dfphi2  12361  hashgcdlem  12379  odzdvds  12386  nnoddn2prm  12401  pythagtriplem1  12406  pceulem  12435  pcqmul  12444  pcqcl  12447  pcxnn0cl  12451  pcxcl  12452  pcneg  12466  pcabs  12467  pcgcd1  12469  pcz  12473  pcprmpw2  12474  pcprmpw  12475  dvdsprmpweqle  12478  difsqpwdvds  12479  pcaddlem  12480  pcadd  12481  pcmpt  12484  pockthg  12498  4sqlem2  12530  4sqlem4  12533  mul4sq  12535  mnd1id  13031  0subm  13059  mulgnn0p1  13206  mulgnn0ass  13231  dvreq1  13641  nzrunit  13687  rrgeq0  13764  domneq0  13771  lmodfopnelem2  13824  lss1d  13882  lspsneq0  13925  znidom  14156  znunit  14158  znrrg  14159  istopon  14192  eltg3  14236  tgidm  14253  restbasg  14347  tgrest  14348  tgcn  14387  cnconst  14413  lmss  14425  txbas  14437  txbasval  14446  upxp  14451  blssps  14606  blss  14607  metrest  14685  blssioo  14732  elcncf1di  14758  elply2  14914  plyf  14916  lgsmod  15183  lgsne0  15195  lgsdirnn0  15204  gausslemma2dlem1a  15215  gausslemma2dlem6  15224  lgseisenlem2  15228  lgsquadlem1  15234  lgsquadlem2  15235  2lgslem1b  15246  2sqlem2  15272  mul2sq  15273  2sqlem7  15278  bj-peano4  15517