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  3626  preqr1g  3767  opth1  4237  euotd  4255  tz7.2  4355  reusv3  4461  alxfr  4462  reuhypd  4472  ordsucim  4500  suc11g  4557  nlimsucg  4566  xpsspw  4739  funcnvuni  5286  fvmptdv2  5606  fsn  5689  fconst2g  5732  funfvima  5749  foco2  5755  isores3  5816  eusvobj2  5861  ovmpodv2  6008  ovelrn  6023  f1opw2  6077  suppssfv  6079  suppssov1  6080  nnmordi  6517  nnmord  6518  qsss  6594  eroveu  6626  th3qlem1  6637  mapsncnv  6695  elixpsn  6735  ixpsnf1o  6736  en1bg  6800  mapxpen  6848  en1eqsnbi  6948  updjud  7081  addnidpig  7335  enq0tr  7433  prcdnql  7483  prcunqu  7484  genipv  7508  genpelvl  7511  genpelvu  7512  distrlem5prl  7585  distrlem5pru  7586  aptiprlemu  7639  mulrid  7954  ltne  8042  cnegex  8135  creur  8916  creui  8917  cju  8918  nnsub  8958  un0addcl  9209  un0mulcl  9210  zaddcl  9293  elz2  9324  qmulz  9623  qre  9625  qnegcl  9636  elpqb  9649  xrltne  9813  xlesubadd  9883  iccid  9925  fzsn  10066  fzsuc2  10079  fz1sbc  10096  elfzp12  10099  modqmuladd  10366  bcval5  10743  bcpasc  10746  hashprg  10788  hashfzo  10802  shftlem  10825  replim  10868  sqrtsq  11053  absle  11098  maxabslemval  11217  negfi  11236  xrmaxiflemval  11258  summodclem2  11390  summodc  11391  zsumdc  11392  fsum3  11395  fsummulc2  11456  fsum00  11470  isumsplit  11499  prodmodclem2  11585  prodmodc  11586  zproddc  11587  fprodseq  11591  prodsnf  11600  fzo0dvdseq  11863  divalgmod  11932  gcdabs1  11990  dvdsgcd  12013  dvdsmulgcd  12026  lcmgcdeq  12083  isprm2lem  12116  dvdsprime  12122  coprm  12144  prmdvdsexpr  12150  rpexp  12153  phibndlem  12216  dfphi2  12220  hashgcdlem  12238  odzdvds  12245  nnoddn2prm  12260  pythagtriplem1  12265  pceulem  12294  pcqmul  12303  pcqcl  12306  pcxnn0cl  12310  pcxcl  12311  pcneg  12324  pcabs  12325  pcgcd1  12327  pcz  12331  pcprmpw2  12332  pcprmpw  12333  dvdsprmpweqle  12336  difsqpwdvds  12337  pcaddlem  12338  pcadd  12339  pcmpt  12341  pockthg  12355  4sqlem2  12387  4sqlem4  12390  mul4sq  12392  mnd1id  12848  0subm  12871  mulgnn0p1  12994  mulgnn0ass  13019  dvreq1  13311  nzrunit  13329  lmodfopnelem2  13415  istopon  13516  eltg3  13560  tgidm  13577  restbasg  13671  tgrest  13672  tgcn  13711  cnconst  13737  lmss  13749  txbas  13761  txbasval  13770  upxp  13775  blssps  13930  blss  13931  metrest  14009  blssioo  14048  elcncf1di  14069  lgsmod  14430  lgsne0  14442  lgsdirnn0  14451  lgseisenlem2  14454  2sqlem2  14465  mul2sq  14466  2sqlem7  14471  bj-peano4  14710