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  3665  preqr1g  3806  opth1  4279  euotd  4298  tz7.2  4400  reusv3  4506  alxfr  4507  reuhypd  4517  ordsucim  4547  suc11g  4604  nlimsucg  4613  xpsspw  4786  funcnvuni  5342  fvmptdv2  5668  fsn  5751  fconst2g  5798  funfvima  5815  foco2  5821  isores3  5883  eusvobj2  5929  ovmpodv2  6078  ovelrn  6094  f1opw2  6151  suppssfv  6153  suppssov1  6154  nnmordi  6601  nnmord  6602  qsss  6680  eroveu  6712  th3qlem1  6723  mapsncnv  6781  elixpsn  6821  ixpsnf1o  6822  en1bg  6891  pw2f1odclem  6930  mapxpen  6944  en1eqsnbi  7050  updjud  7183  addnidpig  7448  enq0tr  7546  prcdnql  7596  prcunqu  7597  genipv  7621  genpelvl  7624  genpelvu  7625  distrlem5prl  7698  distrlem5pru  7699  aptiprlemu  7752  mulrid  8068  ltne  8156  cnegex  8249  creur  9031  creui  9032  cju  9033  nnsub  9074  un0addcl  9327  un0mulcl  9328  zaddcl  9411  elz2  9443  qmulz  9743  qre  9745  qnegcl  9756  elpqb  9770  xrltne  9934  xlesubadd  10004  iccid  10046  fzsn  10187  fzsuc2  10200  fz1sbc  10217  elfzp12  10220  modqmuladd  10509  bcval5  10906  bcpasc  10909  hashprg  10951  hashfzo  10965  wrdl1s1  11082  shftlem  11098  replim  11141  sqrtsq  11326  absle  11371  maxabslemval  11490  negfi  11510  xrmaxiflemval  11532  summodclem2  11664  summodc  11665  zsumdc  11666  fsum3  11669  fsummulc2  11730  fsum00  11744  isumsplit  11773  prodmodclem2  11859  prodmodc  11860  zproddc  11861  fprodseq  11865  prodsnf  11874  fzo0dvdseq  12139  divalgmod  12209  gcdabs1  12281  dvdsgcd  12304  dvdsmulgcd  12317  lcmgcdeq  12376  isprm2lem  12409  dvdsprime  12415  coprm  12437  prmdvdsexpr  12443  rpexp  12446  phibndlem  12509  dfphi2  12513  hashgcdlem  12531  odzdvds  12539  nnoddn2prm  12554  pythagtriplem1  12559  pceulem  12588  pcqmul  12597  pcqcl  12600  pcxnn0cl  12604  pcxcl  12605  pcneg  12619  pcabs  12620  pcgcd1  12622  pcz  12626  pcprmpw2  12627  pcprmpw  12628  dvdsprmpweqle  12631  difsqpwdvds  12632  pcaddlem  12633  pcadd  12634  pcmpt  12637  pockthg  12651  4sqlem2  12683  4sqlem4  12686  mul4sq  12688  mnd1id  13259  0subm  13287  mulgnn0p1  13440  mulgnn0ass  13465  dvreq1  13875  nzrunit  13921  rrgeq0  13998  domneq0  14005  lmodfopnelem2  14058  lss1d  14116  lspsneq0  14159  znidom  14390  znunit  14392  znrrg  14393  istopon  14456  eltg3  14500  tgidm  14517  restbasg  14611  tgrest  14612  tgcn  14651  cnconst  14677  lmss  14689  txbas  14701  txbasval  14710  upxp  14715  blssps  14870  blss  14871  metrest  14949  blssioo  14996  elcncf1di  15022  elply2  15178  plyf  15180  dvdsppwf1o  15432  perfectlem2  15443  perfect  15444  lgsmod  15474  lgsne0  15486  lgsdirnn0  15495  gausslemma2dlem1a  15506  gausslemma2dlem6  15515  lgseisenlem2  15519  lgsquadlem1  15525  lgsquadlem2  15526  2lgslem1b  15537  2sqlem2  15563  mul2sq  15564  2sqlem7  15569  bj-peano4  15853