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  3651  preqr1g  3792  opth1  4265  euotd  4283  tz7.2  4385  reusv3  4491  alxfr  4492  reuhypd  4502  ordsucim  4532  suc11g  4589  nlimsucg  4598  xpsspw  4771  funcnvuni  5323  fvmptdv2  5647  fsn  5730  fconst2g  5773  funfvima  5790  foco2  5796  isores3  5858  eusvobj2  5904  ovmpodv2  6052  ovelrn  6067  f1opw2  6124  suppssfv  6126  suppssov1  6127  nnmordi  6569  nnmord  6570  qsss  6648  eroveu  6680  th3qlem1  6691  mapsncnv  6749  elixpsn  6789  ixpsnf1o  6790  en1bg  6854  pw2f1odclem  6890  mapxpen  6904  en1eqsnbi  7008  updjud  7141  addnidpig  7396  enq0tr  7494  prcdnql  7544  prcunqu  7545  genipv  7569  genpelvl  7572  genpelvu  7573  distrlem5prl  7646  distrlem5pru  7647  aptiprlemu  7700  mulrid  8016  ltne  8104  cnegex  8197  creur  8978  creui  8979  cju  8980  nnsub  9021  un0addcl  9273  un0mulcl  9274  zaddcl  9357  elz2  9388  qmulz  9688  qre  9690  qnegcl  9701  elpqb  9715  xrltne  9879  xlesubadd  9949  iccid  9991  fzsn  10132  fzsuc2  10145  fz1sbc  10162  elfzp12  10165  modqmuladd  10437  bcval5  10834  bcpasc  10837  hashprg  10879  hashfzo  10893  shftlem  10960  replim  11003  sqrtsq  11188  absle  11233  maxabslemval  11352  negfi  11371  xrmaxiflemval  11393  summodclem2  11525  summodc  11526  zsumdc  11527  fsum3  11530  fsummulc2  11591  fsum00  11605  isumsplit  11634  prodmodclem2  11720  prodmodc  11721  zproddc  11722  fprodseq  11726  prodsnf  11735  fzo0dvdseq  11999  divalgmod  12068  gcdabs1  12126  dvdsgcd  12149  dvdsmulgcd  12162  lcmgcdeq  12221  isprm2lem  12254  dvdsprime  12260  coprm  12282  prmdvdsexpr  12288  rpexp  12291  phibndlem  12354  dfphi2  12358  hashgcdlem  12376  odzdvds  12383  nnoddn2prm  12398  pythagtriplem1  12403  pceulem  12432  pcqmul  12441  pcqcl  12444  pcxnn0cl  12448  pcxcl  12449  pcneg  12463  pcabs  12464  pcgcd1  12466  pcz  12470  pcprmpw2  12471  pcprmpw  12472  dvdsprmpweqle  12475  difsqpwdvds  12476  pcaddlem  12477  pcadd  12478  pcmpt  12481  pockthg  12495  4sqlem2  12527  4sqlem4  12530  mul4sq  12532  mnd1id  13028  0subm  13056  mulgnn0p1  13203  mulgnn0ass  13228  dvreq1  13638  nzrunit  13684  rrgeq0  13761  domneq0  13768  lmodfopnelem2  13821  lss1d  13879  lspsneq0  13922  znidom  14145  znunit  14147  znrrg  14148  istopon  14181  eltg3  14225  tgidm  14242  restbasg  14336  tgrest  14337  tgcn  14376  cnconst  14402  lmss  14414  txbas  14426  txbasval  14435  upxp  14440  blssps  14595  blss  14596  metrest  14674  blssioo  14713  elcncf1di  14734  elply2  14881  plyf  14883  lgsmod  15142  lgsne0  15154  lgsdirnn0  15163  gausslemma2dlem1a  15174  gausslemma2dlem6  15183  lgseisenlem2  15187  lgsquadlem1  15191  2sqlem2  15202  mul2sq  15203  2sqlem7  15208  bj-peano4  15447