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  3676  preqr1g  3820  opth1  4298  euotd  4317  tz7.2  4419  reusv3  4525  alxfr  4526  reuhypd  4536  ordsucim  4566  suc11g  4623  nlimsucg  4632  xpsspw  4805  funcnvuni  5362  fvmptdv2  5692  fsn  5775  fconst2g  5822  funfvima  5839  foco2  5845  isores3  5907  eusvobj2  5953  ovmpodv2  6102  ovelrn  6118  f1opw2  6175  suppssfv  6177  suppssov1  6178  nnmordi  6625  nnmord  6626  qsss  6704  eroveu  6736  th3qlem1  6747  mapsncnv  6805  elixpsn  6845  ixpsnf1o  6846  en1bg  6915  pw2f1odclem  6956  mapxpen  6970  en1eqsnbi  7077  updjud  7210  addnidpig  7484  enq0tr  7582  prcdnql  7632  prcunqu  7633  genipv  7657  genpelvl  7660  genpelvu  7661  distrlem5prl  7734  distrlem5pru  7735  aptiprlemu  7788  mulrid  8104  ltne  8192  cnegex  8285  creur  9067  creui  9068  cju  9069  nnsub  9110  un0addcl  9363  un0mulcl  9364  zaddcl  9447  elz2  9479  qmulz  9779  qre  9781  qnegcl  9792  elpqb  9806  xrltne  9970  xlesubadd  10040  iccid  10082  fzsn  10223  fzsuc2  10236  fz1sbc  10253  elfzp12  10256  modqmuladd  10548  bcval5  10945  bcpasc  10948  hashprg  10990  hashfzo  11004  wrdl1s1  11122  cats1un  11212  swrdccat3blem  11230  shftlem  11242  replim  11285  sqrtsq  11470  absle  11515  maxabslemval  11634  negfi  11654  xrmaxiflemval  11676  summodclem2  11808  summodc  11809  zsumdc  11810  fsum3  11813  fsummulc2  11874  fsum00  11888  isumsplit  11917  prodmodclem2  12003  prodmodc  12004  zproddc  12005  fprodseq  12009  prodsnf  12018  fzo0dvdseq  12283  divalgmod  12353  gcdabs1  12425  dvdsgcd  12448  dvdsmulgcd  12461  lcmgcdeq  12520  isprm2lem  12553  dvdsprime  12559  coprm  12581  prmdvdsexpr  12587  rpexp  12590  phibndlem  12653  dfphi2  12657  hashgcdlem  12675  odzdvds  12683  nnoddn2prm  12698  pythagtriplem1  12703  pceulem  12732  pcqmul  12741  pcqcl  12744  pcxnn0cl  12748  pcxcl  12749  pcneg  12763  pcabs  12764  pcgcd1  12766  pcz  12770  pcprmpw2  12771  pcprmpw  12772  dvdsprmpweqle  12775  difsqpwdvds  12776  pcaddlem  12777  pcadd  12778  pcmpt  12781  pockthg  12795  4sqlem2  12827  4sqlem4  12830  mul4sq  12832  mnd1id  13403  0subm  13431  mulgnn0p1  13584  mulgnn0ass  13609  dvreq1  14019  nzrunit  14065  rrgeq0  14142  domneq0  14149  lmodfopnelem2  14202  lss1d  14260  lspsneq0  14303  znidom  14534  znunit  14536  znrrg  14537  istopon  14600  eltg3  14644  tgidm  14661  restbasg  14755  tgrest  14756  tgcn  14795  cnconst  14821  lmss  14833  txbas  14845  txbasval  14854  upxp  14859  blssps  15014  blss  15015  metrest  15093  blssioo  15140  elcncf1di  15166  elply2  15322  plyf  15324  dvdsppwf1o  15576  perfectlem2  15587  perfect  15588  lgsmod  15618  lgsne0  15630  lgsdirnn0  15639  gausslemma2dlem1a  15650  gausslemma2dlem6  15659  lgseisenlem2  15663  lgsquadlem1  15669  lgsquadlem2  15670  2lgslem1b  15681  2sqlem2  15707  mul2sq  15708  2sqlem7  15713  lpvtx  15790  bj-peano4  16090