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  4378  euotd  4397  tz7.2  4501  reusv3  4608  alxfr  4609  reuhypd  4619  ordsucim  4649  suc11g  4706  nlimsucg  4715  xpsspw  4889  funcnvuni  5453  fvmptdv2  5798  fsn  5883  fconst2g  5933  funfvima  5953  foco2  5962  isores3  6024  riotaeqimp  6066  eusvobj2  6074  ovmpodv2  6225  ovelrn  6241  f1opw2  6299  suppssov1  6302  suppssfvg  6507  nnmordi  6794  nnmord  6795  qsss  6873  eroveu  6905  th3qlem1  6916  mapsncnv  6983  elixpsn  7023  ixpsnf1o  7024  en1bg  7093  pw2f1odclem  7140  mapxpen  7154  mapunen  7157  en1eqsnbi  7273  updjud  7428  addnidpig  7709  enq0tr  7807  prcdnql  7857  prcunqu  7858  genipv  7882  genpelvl  7885  genpelvu  7886  distrlem5prl  7959  distrlem5pru  7960  aptiprlemu  8013  mulrid  8329  ltne  8416  cnegex  8511  creur  9297  creui  9298  cju  9299  nnsub  9352  un0addcl  9607  un0mulcl  9608  zaddcl  9693  elz2  9725  qmulz  10038  qre  10040  qnegcl  10051  elpqb  10066  xrltne  10231  xlesubadd  10301  iccid  10343  fzsn  10488  fzsuc2  10502  fz1sbc  10519  elfzp12  10522  modqmuladd  10823  bcval5  11222  bcpasc  11225  hashprg  11270  hashfzo  11284  wrdl1s1  11419  cats1un  11514  swrdccat3blem  11532  shftlem  11602  replim  11645  sqrtsq  11831  absle  11877  maxabslemval  11996  negfi  12016  xrmaxiflemval  12040  summodclem2  12173  summodc  12174  zsumdc  12175  fsum3  12178  fsummulc2  12239  fsum00  12253  isumsplit  12282  prodmodclem2  12368  prodmodc  12369  zproddc  12370  fprodseq  12374  prodsnf  12383  fzo0dvdseq  12648  divalgmod  12718  gcdabs1  12790  dvdsgcd  12813  dvdsmulgcd  12826  lcmgcdeq  12885  isprm2lem  12918  dvdsprime  12924  coprm  12947  prmdvdsexpr  12953  rpexp  12956  phibndlem  13022  dfphi2  13026  hashgcdlem  13044  odzdvds  13052  nnoddn2prm  13067  pythagtriplem1  13072  pceulem  13101  pcqmul  13110  pcqcl  13113  pcxnn0cl  13117  pcxcl  13118  pcneg  13132  pcabs  13133  pcgcd1  13135  pcz  13139  pcprmpw2  13140  pcprmpw  13141  dvdsprmpweqle  13144  difsqpwdvds  13145  pcaddlem  13146  pcadd  13147  pcmpt  13150  pockthg  13164  4sqlem2  13196  4sqlem4  13199  mul4sq  13201  prmlem1a  13249  ballotfilemfc0  13289  ballotfilemfcc  13290  mnd1id  13821  0subm  13849  mulgnn0p1  13994  mulgnn0ass  14019  dvreq1  14557  nzrunit  14603  rrgeq0  14681  domneq0  14689  lmodfopnelem2  14770  lss1d  14828  lspsneq0  14871  gsumfsum  15031  znidom  15100  znunit  15102  znrrg  15103  istopon  15256  eltg3  15300  tgidm  15317  restbasg  15411  tgrest  15412  tgcn  15451  cnconst  15477  lmss  15489  txbas  15501  txbasval  15510  upxp  15515  blssps  15670  blss  15671  metrest  15749  blssioo  15796  elcncf1di  15822  elply2  15978  plyf  15980  efnthr  16193  dvdsppwf1o  16300  ppiublem1  16308  chtublem  16312  perfectlem2  16317  perfect  16318  bposlem1  16328  lgsmod  16367  lgsne0  16379  lgsdirnn0  16388  gausslemma2dlem1a  16399  gausslemma2dlem6  16408  lgseisenlem2  16412  lgsquadlem1  16418  lgsquadlem2  16419  2lgslem1b  16430  2sqlem2  16456  mul2sq  16457  2sqlem7  16462  lpvtx  16542  usgredgop  16636  uhgrspansubgrlem  16739  vtxd0nedgbfi  16762  wlk1walkdom  16822  upgrwlkvtxedg  16827  clwwlkext2edg  16885  clwwlknonccat  16896  bj-peano4  17203