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  3738  preqr1g  3886  opth1  4371  euotd  4390  tz7.2  4494  reusv3  4601  alxfr  4602  reuhypd  4612  ordsucim  4642  suc11g  4699  nlimsucg  4708  xpsspw  4882  funcnvuni  5445  fvmptdv2  5789  fsn  5871  fconst2g  5921  funfvima  5940  foco2  5949  isores3  6011  riotaeqimp  6053  eusvobj2  6061  ovmpodv2  6212  ovelrn  6228  f1opw2  6286  suppssov1  6289  suppssfvg  6493  nnmordi  6779  nnmord  6780  qsss  6858  eroveu  6890  th3qlem1  6901  mapsncnv  6967  elixpsn  7007  ixpsnf1o  7008  en1bg  7077  pw2f1odclem  7124  mapxpen  7138  mapunen  7141  en1eqsnbi  7256  updjud  7412  addnidpig  7693  enq0tr  7791  prcdnql  7841  prcunqu  7842  genipv  7866  genpelvl  7869  genpelvu  7870  distrlem5prl  7943  distrlem5pru  7944  aptiprlemu  7997  mulrid  8313  ltne  8400  cnegex  8494  creur  9279  creui  9280  cju  9281  nnsub  9322  un0addcl  9575  un0mulcl  9576  zaddcl  9663  elz2  9695  qmulz  10002  qre  10004  qnegcl  10015  elpqb  10029  xrltne  10194  xlesubadd  10264  iccid  10306  fzsn  10450  fzsuc2  10464  fz1sbc  10481  elfzp12  10484  modqmuladd  10781  bcval5  11179  bcpasc  11182  hashprg  11227  hashfzo  11241  wrdl1s1  11376  cats1un  11471  swrdccat3blem  11489  shftlem  11559  replim  11602  sqrtsq  11788  absle  11833  maxabslemval  11952  negfi  11972  xrmaxiflemval  11994  summodclem2  12127  summodc  12128  zsumdc  12129  fsum3  12132  fsummulc2  12193  fsum00  12207  isumsplit  12236  prodmodclem2  12322  prodmodc  12323  zproddc  12324  fprodseq  12328  prodsnf  12337  fzo0dvdseq  12602  divalgmod  12672  gcdabs1  12744  dvdsgcd  12767  dvdsmulgcd  12780  lcmgcdeq  12839  isprm2lem  12872  dvdsprime  12878  coprm  12900  prmdvdsexpr  12906  rpexp  12909  phibndlem  12972  dfphi2  12976  hashgcdlem  12994  odzdvds  13002  nnoddn2prm  13017  pythagtriplem1  13022  pceulem  13051  pcqmul  13060  pcqcl  13063  pcxnn0cl  13067  pcxcl  13068  pcneg  13082  pcabs  13083  pcgcd1  13085  pcz  13089  pcprmpw2  13090  pcprmpw  13091  dvdsprmpweqle  13094  difsqpwdvds  13095  pcaddlem  13096  pcadd  13097  pcmpt  13100  pockthg  13114  4sqlem2  13146  4sqlem4  13149  mul4sq  13151  ballotfilemfc0  13210  ballotfilemfcc  13211  mnd1id  13740  0subm  13768  mulgnn0p1  13913  mulgnn0ass  13938  dvreq1  14422  nzrunit  14468  rrgeq0  14546  domneq0  14554  lmodfopnelem2  14634  lss1d  14692  lspsneq0  14735  gsumfsum  14895  znidom  14964  znunit  14966  znrrg  14967  istopon  15037  eltg3  15081  tgidm  15098  restbasg  15192  tgrest  15193  tgcn  15232  cnconst  15258  lmss  15270  txbas  15282  txbasval  15291  upxp  15296  blssps  15451  blss  15452  metrest  15530  blssioo  15577  elcncf1di  15603  elply2  15759  plyf  15761  dvdsppwf1o  16017  perfectlem2  16028  perfect  16029  lgsmod  16059  lgsne0  16071  lgsdirnn0  16080  gausslemma2dlem1a  16091  gausslemma2dlem6  16100  lgseisenlem2  16104  lgsquadlem1  16110  lgsquadlem2  16111  2lgslem1b  16122  2sqlem2  16148  mul2sq  16149  2sqlem7  16154  lpvtx  16234  usgredgop  16328  uhgrspansubgrlem  16431  vtxd0nedgbfi  16454  wlk1walkdom  16514  upgrwlkvtxedg  16519  clwwlkext2edg  16577  clwwlknonccat  16588  bj-peano4  16895