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  3656  preqr1g  3797  opth1  4270  euotd  4288  tz7.2  4390  reusv3  4496  alxfr  4497  reuhypd  4507  ordsucim  4537  suc11g  4594  nlimsucg  4603  xpsspw  4776  funcnvuni  5328  fvmptdv2  5652  fsn  5735  fconst2g  5778  funfvima  5795  foco2  5801  isores3  5863  eusvobj2  5909  ovmpodv2  6058  ovelrn  6074  f1opw2  6131  suppssfv  6133  suppssov1  6134  nnmordi  6576  nnmord  6577  qsss  6655  eroveu  6687  th3qlem1  6698  mapsncnv  6756  elixpsn  6796  ixpsnf1o  6797  en1bg  6861  pw2f1odclem  6897  mapxpen  6911  en1eqsnbi  7017  updjud  7150  addnidpig  7406  enq0tr  7504  prcdnql  7554  prcunqu  7555  genipv  7579  genpelvl  7582  genpelvu  7583  distrlem5prl  7656  distrlem5pru  7657  aptiprlemu  7710  mulrid  8026  ltne  8114  cnegex  8207  creur  8989  creui  8990  cju  8991  nnsub  9032  un0addcl  9285  un0mulcl  9286  zaddcl  9369  elz2  9400  qmulz  9700  qre  9702  qnegcl  9713  elpqb  9727  xrltne  9891  xlesubadd  9961  iccid  10003  fzsn  10144  fzsuc2  10157  fz1sbc  10174  elfzp12  10177  modqmuladd  10461  bcval5  10858  bcpasc  10861  hashprg  10903  hashfzo  10917  shftlem  10984  replim  11027  sqrtsq  11212  absle  11257  maxabslemval  11376  negfi  11396  xrmaxiflemval  11418  summodclem2  11550  summodc  11551  zsumdc  11552  fsum3  11555  fsummulc2  11616  fsum00  11630  isumsplit  11659  prodmodclem2  11745  prodmodc  11746  zproddc  11747  fprodseq  11751  prodsnf  11760  fzo0dvdseq  12025  divalgmod  12095  gcdabs1  12167  dvdsgcd  12190  dvdsmulgcd  12203  lcmgcdeq  12262  isprm2lem  12295  dvdsprime  12301  coprm  12323  prmdvdsexpr  12329  rpexp  12332  phibndlem  12395  dfphi2  12399  hashgcdlem  12417  odzdvds  12425  nnoddn2prm  12440  pythagtriplem1  12445  pceulem  12474  pcqmul  12483  pcqcl  12486  pcxnn0cl  12490  pcxcl  12491  pcneg  12505  pcabs  12506  pcgcd1  12508  pcz  12512  pcprmpw2  12513  pcprmpw  12514  dvdsprmpweqle  12517  difsqpwdvds  12518  pcaddlem  12519  pcadd  12520  pcmpt  12523  pockthg  12537  4sqlem2  12569  4sqlem4  12572  mul4sq  12574  mnd1id  13114  0subm  13142  mulgnn0p1  13289  mulgnn0ass  13314  dvreq1  13724  nzrunit  13770  rrgeq0  13847  domneq0  13854  lmodfopnelem2  13907  lss1d  13965  lspsneq0  14008  znidom  14239  znunit  14241  znrrg  14242  istopon  14275  eltg3  14319  tgidm  14336  restbasg  14430  tgrest  14431  tgcn  14470  cnconst  14496  lmss  14508  txbas  14520  txbasval  14529  upxp  14534  blssps  14689  blss  14690  metrest  14768  blssioo  14815  elcncf1di  14841  elply2  14997  plyf  14999  dvdsppwf1o  15251  perfectlem2  15262  perfect  15263  lgsmod  15293  lgsne0  15305  lgsdirnn0  15314  gausslemma2dlem1a  15325  gausslemma2dlem6  15334  lgseisenlem2  15338  lgsquadlem1  15344  lgsquadlem2  15345  2lgslem1b  15356  2sqlem2  15382  mul2sq  15383  2sqlem7  15388  bj-peano4  15627