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  4376  euotd  4395  tz7.2  4499  reusv3  4606  alxfr  4607  reuhypd  4617  ordsucim  4647  suc11g  4704  nlimsucg  4713  xpsspw  4887  funcnvuni  5450  fvmptdv2  5795  fsn  5880  fconst2g  5930  funfvima  5950  foco2  5959  isores3  6021  riotaeqimp  6063  eusvobj2  6071  ovmpodv2  6222  ovelrn  6238  f1opw2  6296  suppssov1  6299  suppssfvg  6503  nnmordi  6789  nnmord  6790  qsss  6868  eroveu  6900  th3qlem1  6911  mapsncnv  6977  elixpsn  7017  ixpsnf1o  7018  en1bg  7087  pw2f1odclem  7134  mapxpen  7148  mapunen  7151  en1eqsnbi  7266  updjud  7422  addnidpig  7703  enq0tr  7801  prcdnql  7851  prcunqu  7852  genipv  7876  genpelvl  7879  genpelvu  7880  distrlem5prl  7953  distrlem5pru  7954  aptiprlemu  8007  mulrid  8323  ltne  8410  cnegex  8505  creur  9291  creui  9292  cju  9293  nnsub  9345  un0addcl  9600  un0mulcl  9601  zaddcl  9688  elz2  9720  qmulz  10032  qre  10034  qnegcl  10045  elpqb  10060  xrltne  10225  xlesubadd  10295  iccid  10337  fzsn  10482  fzsuc2  10496  fz1sbc  10513  elfzp12  10516  modqmuladd  10816  bcval5  11215  bcpasc  11218  hashprg  11263  hashfzo  11277  wrdl1s1  11412  cats1un  11507  swrdccat3blem  11525  shftlem  11595  replim  11638  sqrtsq  11824  absle  11870  maxabslemval  11989  negfi  12009  xrmaxiflemval  12032  summodclem2  12165  summodc  12166  zsumdc  12167  fsum3  12170  fsummulc2  12231  fsum00  12245  isumsplit  12274  prodmodclem2  12360  prodmodc  12361  zproddc  12362  fprodseq  12366  prodsnf  12375  fzo0dvdseq  12640  divalgmod  12710  gcdabs1  12782  dvdsgcd  12805  dvdsmulgcd  12818  lcmgcdeq  12877  isprm2lem  12910  dvdsprime  12916  coprm  12939  prmdvdsexpr  12945  rpexp  12948  phibndlem  13014  dfphi2  13018  hashgcdlem  13036  odzdvds  13044  nnoddn2prm  13059  pythagtriplem1  13064  pceulem  13093  pcqmul  13102  pcqcl  13105  pcxnn0cl  13109  pcxcl  13110  pcneg  13124  pcabs  13125  pcgcd1  13127  pcz  13131  pcprmpw2  13132  pcprmpw  13133  dvdsprmpweqle  13136  difsqpwdvds  13137  pcaddlem  13138  pcadd  13139  pcmpt  13142  pockthg  13156  4sqlem2  13188  4sqlem4  13191  mul4sq  13193  prmlem1a  13241  ballotfilemfc0  13281  ballotfilemfcc  13282  mnd1id  13812  0subm  13840  mulgnn0p1  13985  mulgnn0ass  14010  dvreq1  14498  nzrunit  14544  rrgeq0  14622  domneq0  14630  lmodfopnelem2  14711  lss1d  14769  lspsneq0  14812  gsumfsum  14972  znidom  15041  znunit  15043  znrrg  15044  istopon  15163  eltg3  15207  tgidm  15224  restbasg  15318  tgrest  15319  tgcn  15358  cnconst  15384  lmss  15396  txbas  15408  txbasval  15417  upxp  15422  blssps  15577  blss  15578  metrest  15656  blssioo  15703  elcncf1di  15729  elply2  15885  plyf  15887  dvdsppwf1o  16184  ppiublem1  16192  perfectlem2  16198  perfect  16199  bposlem1  16209  lgsmod  16243  lgsne0  16255  lgsdirnn0  16264  gausslemma2dlem1a  16275  gausslemma2dlem6  16284  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  2lgslem1b  16306  2sqlem2  16332  mul2sq  16333  2sqlem7  16338  lpvtx  16418  usgredgop  16512  uhgrspansubgrlem  16615  vtxd0nedgbfi  16638  wlk1walkdom  16698  upgrwlkvtxedg  16703  clwwlkext2edg  16761  clwwlknonccat  16772  bj-peano4  17079