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  3700  preqr1g  3847  opth1  4326  euotd  4345  tz7.2  4449  reusv3  4555  alxfr  4556  reuhypd  4566  ordsucim  4596  suc11g  4653  nlimsucg  4662  xpsspw  4836  funcnvuni  5396  fvmptdv2  5732  fsn  5815  fconst2g  5864  funfvima  5881  foco2  5889  isores3  5951  riotaeqimp  5991  eusvobj2  5999  ovmpodv2  6150  ovelrn  6166  f1opw2  6224  suppssfv  6226  suppssov1  6227  nnmordi  6679  nnmord  6680  qsss  6758  eroveu  6790  th3qlem1  6801  mapsncnv  6859  elixpsn  6899  ixpsnf1o  6900  en1bg  6969  pw2f1odclem  7015  mapxpen  7029  en1eqsnbi  7139  updjud  7272  addnidpig  7546  enq0tr  7644  prcdnql  7694  prcunqu  7695  genipv  7719  genpelvl  7722  genpelvu  7723  distrlem5prl  7796  distrlem5pru  7797  aptiprlemu  7850  mulrid  8166  ltne  8254  cnegex  8347  creur  9129  creui  9130  cju  9131  nnsub  9172  un0addcl  9425  un0mulcl  9426  zaddcl  9509  elz2  9541  qmulz  9847  qre  9849  qnegcl  9860  elpqb  9874  xrltne  10038  xlesubadd  10108  iccid  10150  fzsn  10291  fzsuc2  10304  fz1sbc  10321  elfzp12  10324  modqmuladd  10618  bcval5  11015  bcpasc  11018  hashprg  11062  hashfzo  11076  wrdl1s1  11197  cats1un  11292  swrdccat3blem  11310  shftlem  11367  replim  11410  sqrtsq  11595  absle  11640  maxabslemval  11759  negfi  11779  xrmaxiflemval  11801  summodclem2  11933  summodc  11934  zsumdc  11935  fsum3  11938  fsummulc2  11999  fsum00  12013  isumsplit  12042  prodmodclem2  12128  prodmodc  12129  zproddc  12130  fprodseq  12134  prodsnf  12143  fzo0dvdseq  12408  divalgmod  12478  gcdabs1  12550  dvdsgcd  12573  dvdsmulgcd  12586  lcmgcdeq  12645  isprm2lem  12678  dvdsprime  12684  coprm  12706  prmdvdsexpr  12712  rpexp  12715  phibndlem  12778  dfphi2  12782  hashgcdlem  12800  odzdvds  12808  nnoddn2prm  12823  pythagtriplem1  12828  pceulem  12857  pcqmul  12866  pcqcl  12869  pcxnn0cl  12873  pcxcl  12874  pcneg  12888  pcabs  12889  pcgcd1  12891  pcz  12895  pcprmpw2  12896  pcprmpw  12897  dvdsprmpweqle  12900  difsqpwdvds  12901  pcaddlem  12902  pcadd  12903  pcmpt  12906  pockthg  12920  4sqlem2  12952  4sqlem4  12955  mul4sq  12957  mnd1id  13529  0subm  13557  mulgnn0p1  13710  mulgnn0ass  13735  dvreq1  14146  nzrunit  14192  rrgeq0  14269  domneq0  14276  lmodfopnelem2  14329  lss1d  14387  lspsneq0  14430  znidom  14661  znunit  14663  znrrg  14664  istopon  14727  eltg3  14771  tgidm  14788  restbasg  14882  tgrest  14883  tgcn  14922  cnconst  14948  lmss  14960  txbas  14972  txbasval  14981  upxp  14986  blssps  15141  blss  15142  metrest  15220  blssioo  15267  elcncf1di  15293  elply2  15449  plyf  15451  dvdsppwf1o  15703  perfectlem2  15714  perfect  15715  lgsmod  15745  lgsne0  15757  lgsdirnn0  15766  gausslemma2dlem1a  15777  gausslemma2dlem6  15786  lgseisenlem2  15790  lgsquadlem1  15796  lgsquadlem2  15797  2lgslem1b  15808  2sqlem2  15834  mul2sq  15835  2sqlem7  15840  lpvtx  15920  usgredgop  16012  vtxd0nedgbfi  16105  wlk1walkdom  16156  upgrwlkvtxedg  16161  clwwlkext2edg  16217  clwwlknonccat  16228  bj-peano4  16486