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  3706  preqr1g  3854  opth1  4334  euotd  4353  tz7.2  4457  reusv3  4563  alxfr  4564  reuhypd  4574  ordsucim  4604  suc11g  4661  nlimsucg  4670  xpsspw  4844  funcnvuni  5406  fvmptdv2  5745  fsn  5827  fconst2g  5877  funfvima  5896  foco2  5904  isores3  5966  riotaeqimp  6006  eusvobj2  6014  ovmpodv2  6165  ovelrn  6181  f1opw2  6239  suppssov1  6241  suppssfvg  6441  nnmordi  6727  nnmord  6728  qsss  6806  eroveu  6838  th3qlem1  6849  mapsncnv  6907  elixpsn  6947  ixpsnf1o  6948  en1bg  7017  pw2f1odclem  7063  mapxpen  7077  en1eqsnbi  7191  updjud  7324  addnidpig  7599  enq0tr  7697  prcdnql  7747  prcunqu  7748  genipv  7772  genpelvl  7775  genpelvu  7776  distrlem5prl  7849  distrlem5pru  7850  aptiprlemu  7903  mulrid  8219  ltne  8306  cnegex  8399  creur  9181  creui  9182  cju  9183  nnsub  9224  un0addcl  9477  un0mulcl  9478  zaddcl  9563  elz2  9595  qmulz  9901  qre  9903  qnegcl  9914  elpqb  9928  xrltne  10092  xlesubadd  10162  iccid  10204  fzsn  10346  fzsuc2  10359  fz1sbc  10376  elfzp12  10379  modqmuladd  10674  bcval5  11071  bcpasc  11074  hashprg  11118  hashfzo  11132  wrdl1s1  11256  cats1un  11351  swrdccat3blem  11369  shftlem  11439  replim  11482  sqrtsq  11667  absle  11712  maxabslemval  11831  negfi  11851  xrmaxiflemval  11873  summodclem2  12006  summodc  12007  zsumdc  12008  fsum3  12011  fsummulc2  12072  fsum00  12086  isumsplit  12115  prodmodclem2  12201  prodmodc  12202  zproddc  12203  fprodseq  12207  prodsnf  12216  fzo0dvdseq  12481  divalgmod  12551  gcdabs1  12623  dvdsgcd  12646  dvdsmulgcd  12659  lcmgcdeq  12718  isprm2lem  12751  dvdsprime  12757  coprm  12779  prmdvdsexpr  12785  rpexp  12788  phibndlem  12851  dfphi2  12855  hashgcdlem  12873  odzdvds  12881  nnoddn2prm  12896  pythagtriplem1  12901  pceulem  12930  pcqmul  12939  pcqcl  12942  pcxnn0cl  12946  pcxcl  12947  pcneg  12961  pcabs  12962  pcgcd1  12964  pcz  12968  pcprmpw2  12969  pcprmpw  12970  dvdsprmpweqle  12973  difsqpwdvds  12974  pcaddlem  12975  pcadd  12976  pcmpt  12979  pockthg  12993  4sqlem2  13025  4sqlem4  13028  mul4sq  13030  mnd1id  13602  0subm  13630  mulgnn0p1  13783  mulgnn0ass  13808  dvreq1  14220  nzrunit  14266  rrgeq0  14343  domneq0  14351  lmodfopnelem2  14404  lss1d  14462  lspsneq0  14505  znidom  14736  znunit  14738  znrrg  14739  istopon  14807  eltg3  14851  tgidm  14868  restbasg  14962  tgrest  14963  tgcn  15002  cnconst  15028  lmss  15040  txbas  15052  txbasval  15061  upxp  15066  blssps  15221  blss  15222  metrest  15300  blssioo  15347  elcncf1di  15373  elply2  15529  plyf  15531  dvdsppwf1o  15786  perfectlem2  15797  perfect  15798  lgsmod  15828  lgsne0  15840  lgsdirnn0  15849  gausslemma2dlem1a  15860  gausslemma2dlem6  15869  lgseisenlem2  15873  lgsquadlem1  15879  lgsquadlem2  15880  2lgslem1b  15891  2sqlem2  15917  mul2sq  15918  2sqlem7  15923  lpvtx  16003  usgredgop  16097  uhgrspansubgrlem  16200  vtxd0nedgbfi  16223  wlk1walkdom  16283  upgrwlkvtxedg  16288  clwwlkext2edg  16346  clwwlknonccat  16357  bj-peano4  16654