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  3724  preqr1g  3872  opth1  4354  euotd  4373  tz7.2  4477  reusv3  4583  alxfr  4584  reuhypd  4594  ordsucim  4624  suc11g  4681  nlimsucg  4690  xpsspw  4864  funcnvuni  5427  fvmptdv2  5769  fsn  5851  fconst2g  5901  funfvima  5920  foco2  5928  isores3  5990  riotaeqimp  6030  eusvobj2  6038  ovmpodv2  6189  ovelrn  6205  f1opw2  6263  suppssov1  6265  suppssfvg  6465  nnmordi  6751  nnmord  6752  qsss  6830  eroveu  6862  th3qlem1  6873  mapsncnv  6932  elixpsn  6972  ixpsnf1o  6973  en1bg  7042  pw2f1odclem  7089  mapxpen  7103  mapunen  7106  en1eqsnbi  7221  updjud  7375  addnidpig  7653  enq0tr  7751  prcdnql  7801  prcunqu  7802  genipv  7826  genpelvl  7829  genpelvu  7830  distrlem5prl  7903  distrlem5pru  7904  aptiprlemu  7957  mulrid  8273  ltne  8360  cnegex  8453  creur  9235  creui  9236  cju  9237  nnsub  9278  un0addcl  9531  un0mulcl  9532  zaddcl  9619  elz2  9651  qmulz  9958  qre  9960  qnegcl  9971  elpqb  9985  xrltne  10149  xlesubadd  10219  iccid  10261  fzsn  10403  fzsuc2  10417  fz1sbc  10434  elfzp12  10437  modqmuladd  10732  bcval5  11129  bcpasc  11132  hashprg  11177  hashfzo  11191  wrdl1s1  11322  cats1un  11417  swrdccat3blem  11435  shftlem  11505  replim  11548  sqrtsq  11733  absle  11778  maxabslemval  11897  negfi  11917  xrmaxiflemval  11939  summodclem2  12072  summodc  12073  zsumdc  12074  fsum3  12077  fsummulc2  12138  fsum00  12152  isumsplit  12181  prodmodclem2  12267  prodmodc  12268  zproddc  12269  fprodseq  12273  prodsnf  12282  fzo0dvdseq  12547  divalgmod  12617  gcdabs1  12689  dvdsgcd  12712  dvdsmulgcd  12725  lcmgcdeq  12784  isprm2lem  12817  dvdsprime  12823  coprm  12845  prmdvdsexpr  12851  rpexp  12854  phibndlem  12917  dfphi2  12921  hashgcdlem  12939  odzdvds  12947  nnoddn2prm  12962  pythagtriplem1  12967  pceulem  12996  pcqmul  13005  pcqcl  13008  pcxnn0cl  13012  pcxcl  13013  pcneg  13027  pcabs  13028  pcgcd1  13030  pcz  13034  pcprmpw2  13035  pcprmpw  13036  dvdsprmpweqle  13039  difsqpwdvds  13040  pcaddlem  13041  pcadd  13042  pcmpt  13045  pockthg  13059  4sqlem2  13091  4sqlem4  13094  mul4sq  13096  ballotfilemfc0  13153  ballotfilemfcc  13154  mnd1id  13686  0subm  13714  mulgnn0p1  13867  mulgnn0ass  13892  dvreq1  14304  nzrunit  14350  rrgeq0  14427  domneq0  14435  lmodfopnelem2  14490  lss1d  14548  lspsneq0  14591  znidom  14822  znunit  14824  znrrg  14825  istopon  14895  eltg3  14939  tgidm  14956  restbasg  15050  tgrest  15051  tgcn  15090  cnconst  15116  lmss  15128  txbas  15140  txbasval  15149  upxp  15154  blssps  15309  blss  15310  metrest  15388  blssioo  15435  elcncf1di  15461  elply2  15617  plyf  15619  dvdsppwf1o  15874  perfectlem2  15885  perfect  15886  lgsmod  15916  lgsne0  15928  lgsdirnn0  15937  gausslemma2dlem1a  15948  gausslemma2dlem6  15957  lgseisenlem2  15961  lgsquadlem1  15967  lgsquadlem2  15968  2lgslem1b  15979  2sqlem2  16005  mul2sq  16006  2sqlem7  16011  lpvtx  16091  usgredgop  16185  uhgrspansubgrlem  16288  vtxd0nedgbfi  16311  wlk1walkdom  16371  upgrwlkvtxedg  16376  clwwlkext2edg  16434  clwwlknonccat  16445  bj-peano4  16742