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  3702  preqr1g  3849  opth1  4328  euotd  4347  tz7.2  4451  reusv3  4557  alxfr  4558  reuhypd  4568  ordsucim  4598  suc11g  4655  nlimsucg  4664  xpsspw  4838  funcnvuni  5399  fvmptdv2  5736  fsn  5819  fconst2g  5868  funfvima  5885  foco2  5893  isores3  5955  riotaeqimp  5995  eusvobj2  6003  ovmpodv2  6154  ovelrn  6170  f1opw2  6228  suppssfv  6230  suppssov1  6231  nnmordi  6683  nnmord  6684  qsss  6762  eroveu  6794  th3qlem1  6805  mapsncnv  6863  elixpsn  6903  ixpsnf1o  6904  en1bg  6973  pw2f1odclem  7019  mapxpen  7033  en1eqsnbi  7147  updjud  7280  addnidpig  7555  enq0tr  7653  prcdnql  7703  prcunqu  7704  genipv  7728  genpelvl  7731  genpelvu  7732  distrlem5prl  7805  distrlem5pru  7806  aptiprlemu  7859  mulrid  8175  ltne  8263  cnegex  8356  creur  9138  creui  9139  cju  9140  nnsub  9181  un0addcl  9434  un0mulcl  9435  zaddcl  9518  elz2  9550  qmulz  9856  qre  9858  qnegcl  9869  elpqb  9883  xrltne  10047  xlesubadd  10117  iccid  10159  fzsn  10300  fzsuc2  10313  fz1sbc  10330  elfzp12  10333  modqmuladd  10627  bcval5  11024  bcpasc  11027  hashprg  11071  hashfzo  11085  wrdl1s1  11206  cats1un  11301  swrdccat3blem  11319  shftlem  11376  replim  11419  sqrtsq  11604  absle  11649  maxabslemval  11768  negfi  11788  xrmaxiflemval  11810  summodclem2  11942  summodc  11943  zsumdc  11944  fsum3  11947  fsummulc2  12008  fsum00  12022  isumsplit  12051  prodmodclem2  12137  prodmodc  12138  zproddc  12139  fprodseq  12143  prodsnf  12152  fzo0dvdseq  12417  divalgmod  12487  gcdabs1  12559  dvdsgcd  12582  dvdsmulgcd  12595  lcmgcdeq  12654  isprm2lem  12687  dvdsprime  12693  coprm  12715  prmdvdsexpr  12721  rpexp  12724  phibndlem  12787  dfphi2  12791  hashgcdlem  12809  odzdvds  12817  nnoddn2prm  12832  pythagtriplem1  12837  pceulem  12866  pcqmul  12875  pcqcl  12878  pcxnn0cl  12882  pcxcl  12883  pcneg  12897  pcabs  12898  pcgcd1  12900  pcz  12904  pcprmpw2  12905  pcprmpw  12906  dvdsprmpweqle  12909  difsqpwdvds  12910  pcaddlem  12911  pcadd  12912  pcmpt  12915  pockthg  12929  4sqlem2  12961  4sqlem4  12964  mul4sq  12966  mnd1id  13538  0subm  13566  mulgnn0p1  13719  mulgnn0ass  13744  dvreq1  14155  nzrunit  14201  rrgeq0  14278  domneq0  14285  lmodfopnelem2  14338  lss1d  14396  lspsneq0  14439  znidom  14670  znunit  14672  znrrg  14673  istopon  14736  eltg3  14780  tgidm  14797  restbasg  14891  tgrest  14892  tgcn  14931  cnconst  14957  lmss  14969  txbas  14981  txbasval  14990  upxp  14995  blssps  15150  blss  15151  metrest  15229  blssioo  15276  elcncf1di  15302  elply2  15458  plyf  15460  dvdsppwf1o  15712  perfectlem2  15723  perfect  15724  lgsmod  15754  lgsne0  15766  lgsdirnn0  15775  gausslemma2dlem1a  15786  gausslemma2dlem6  15795  lgseisenlem2  15799  lgsquadlem1  15805  lgsquadlem2  15806  2lgslem1b  15817  2sqlem2  15843  mul2sq  15844  2sqlem7  15849  lpvtx  15929  usgredgop  16023  uhgrspansubgrlem  16126  vtxd0nedgbfi  16149  wlk1walkdom  16209  upgrwlkvtxedg  16214  clwwlkext2edg  16272  clwwlknonccat  16283  bj-peano4  16550