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  3656  preqr1g  3797  opth1  4270  euotd  4288  tz7.2  4390  reusv3  4496  alxfr  4497  reuhypd  4507  ordsucim  4537  suc11g  4594  nlimsucg  4603  xpsspw  4776  funcnvuni  5328  fvmptdv2  5654  fsn  5737  fconst2g  5780  funfvima  5797  foco2  5803  isores3  5865  eusvobj2  5911  ovmpodv2  6060  ovelrn  6076  f1opw2  6133  suppssfv  6135  suppssov1  6136  nnmordi  6583  nnmord  6584  qsss  6662  eroveu  6694  th3qlem1  6705  mapsncnv  6763  elixpsn  6803  ixpsnf1o  6804  en1bg  6868  pw2f1odclem  6904  mapxpen  6918  en1eqsnbi  7024  updjud  7157  addnidpig  7420  enq0tr  7518  prcdnql  7568  prcunqu  7569  genipv  7593  genpelvl  7596  genpelvu  7597  distrlem5prl  7670  distrlem5pru  7671  aptiprlemu  7724  mulrid  8040  ltne  8128  cnegex  8221  creur  9003  creui  9004  cju  9005  nnsub  9046  un0addcl  9299  un0mulcl  9300  zaddcl  9383  elz2  9414  qmulz  9714  qre  9716  qnegcl  9727  elpqb  9741  xrltne  9905  xlesubadd  9975  iccid  10017  fzsn  10158  fzsuc2  10171  fz1sbc  10188  elfzp12  10191  modqmuladd  10475  bcval5  10872  bcpasc  10875  hashprg  10917  hashfzo  10931  shftlem  10998  replim  11041  sqrtsq  11226  absle  11271  maxabslemval  11390  negfi  11410  xrmaxiflemval  11432  summodclem2  11564  summodc  11565  zsumdc  11566  fsum3  11569  fsummulc2  11630  fsum00  11644  isumsplit  11673  prodmodclem2  11759  prodmodc  11760  zproddc  11761  fprodseq  11765  prodsnf  11774  fzo0dvdseq  12039  divalgmod  12109  gcdabs1  12181  dvdsgcd  12204  dvdsmulgcd  12217  lcmgcdeq  12276  isprm2lem  12309  dvdsprime  12315  coprm  12337  prmdvdsexpr  12343  rpexp  12346  phibndlem  12409  dfphi2  12413  hashgcdlem  12431  odzdvds  12439  nnoddn2prm  12454  pythagtriplem1  12459  pceulem  12488  pcqmul  12497  pcqcl  12500  pcxnn0cl  12504  pcxcl  12505  pcneg  12519  pcabs  12520  pcgcd1  12522  pcz  12526  pcprmpw2  12527  pcprmpw  12528  dvdsprmpweqle  12531  difsqpwdvds  12532  pcaddlem  12533  pcadd  12534  pcmpt  12537  pockthg  12551  4sqlem2  12583  4sqlem4  12586  mul4sq  12588  mnd1id  13158  0subm  13186  mulgnn0p1  13339  mulgnn0ass  13364  dvreq1  13774  nzrunit  13820  rrgeq0  13897  domneq0  13904  lmodfopnelem2  13957  lss1d  14015  lspsneq0  14058  znidom  14289  znunit  14291  znrrg  14292  istopon  14333  eltg3  14377  tgidm  14394  restbasg  14488  tgrest  14489  tgcn  14528  cnconst  14554  lmss  14566  txbas  14578  txbasval  14587  upxp  14592  blssps  14747  blss  14748  metrest  14826  blssioo  14873  elcncf1di  14899  elply2  15055  plyf  15057  dvdsppwf1o  15309  perfectlem2  15320  perfect  15321  lgsmod  15351  lgsne0  15363  lgsdirnn0  15372  gausslemma2dlem1a  15383  gausslemma2dlem6  15392  lgseisenlem2  15396  lgsquadlem1  15402  lgsquadlem2  15403  2lgslem1b  15414  2sqlem2  15440  mul2sq  15441  2sqlem7  15446  bj-peano4  15685