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  3627  preqr1g  3768  opth1  4238  euotd  4256  tz7.2  4356  reusv3  4462  alxfr  4463  reuhypd  4473  ordsucim  4501  suc11g  4558  nlimsucg  4567  xpsspw  4740  funcnvuni  5287  fvmptdv2  5607  fsn  5690  fconst2g  5733  funfvima  5750  foco2  5756  isores3  5818  eusvobj2  5863  ovmpodv2  6010  ovelrn  6025  f1opw2  6079  suppssfv  6081  suppssov1  6082  nnmordi  6519  nnmord  6520  qsss  6596  eroveu  6628  th3qlem1  6639  mapsncnv  6697  elixpsn  6737  ixpsnf1o  6738  en1bg  6802  mapxpen  6850  en1eqsnbi  6950  updjud  7083  addnidpig  7337  enq0tr  7435  prcdnql  7485  prcunqu  7486  genipv  7510  genpelvl  7513  genpelvu  7514  distrlem5prl  7587  distrlem5pru  7588  aptiprlemu  7641  mulrid  7956  ltne  8044  cnegex  8137  creur  8918  creui  8919  cju  8920  nnsub  8960  un0addcl  9211  un0mulcl  9212  zaddcl  9295  elz2  9326  qmulz  9625  qre  9627  qnegcl  9638  elpqb  9651  xrltne  9815  xlesubadd  9885  iccid  9927  fzsn  10068  fzsuc2  10081  fz1sbc  10098  elfzp12  10101  modqmuladd  10368  bcval5  10745  bcpasc  10748  hashprg  10790  hashfzo  10804  shftlem  10827  replim  10870  sqrtsq  11055  absle  11100  maxabslemval  11219  negfi  11238  xrmaxiflemval  11260  summodclem2  11392  summodc  11393  zsumdc  11394  fsum3  11397  fsummulc2  11458  fsum00  11472  isumsplit  11501  prodmodclem2  11587  prodmodc  11588  zproddc  11589  fprodseq  11593  prodsnf  11602  fzo0dvdseq  11865  divalgmod  11934  gcdabs1  11992  dvdsgcd  12015  dvdsmulgcd  12028  lcmgcdeq  12085  isprm2lem  12118  dvdsprime  12124  coprm  12146  prmdvdsexpr  12152  rpexp  12155  phibndlem  12218  dfphi2  12222  hashgcdlem  12240  odzdvds  12247  nnoddn2prm  12262  pythagtriplem1  12267  pceulem  12296  pcqmul  12305  pcqcl  12308  pcxnn0cl  12312  pcxcl  12313  pcneg  12326  pcabs  12327  pcgcd1  12329  pcz  12333  pcprmpw2  12334  pcprmpw  12335  dvdsprmpweqle  12338  difsqpwdvds  12339  pcaddlem  12340  pcadd  12341  pcmpt  12343  pockthg  12357  4sqlem2  12389  4sqlem4  12392  mul4sq  12394  mnd1id  12853  0subm  12876  mulgnn0p1  12999  mulgnn0ass  13024  dvreq1  13316  nzrunit  13334  lmodfopnelem2  13420  lss1d  13475  lspsneq0  13517  istopon  13598  eltg3  13642  tgidm  13659  restbasg  13753  tgrest  13754  tgcn  13793  cnconst  13819  lmss  13831  txbas  13843  txbasval  13852  upxp  13857  blssps  14012  blss  14013  metrest  14091  blssioo  14130  elcncf1di  14151  lgsmod  14512  lgsne0  14524  lgsdirnn0  14533  lgseisenlem2  14536  2sqlem2  14547  mul2sq  14548  2sqlem7  14553  bj-peano4  14792