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  3722  preqr1g  3870  opth1  4352  euotd  4371  tz7.2  4475  reusv3  4581  alxfr  4582  reuhypd  4592  ordsucim  4622  suc11g  4679  nlimsucg  4688  xpsspw  4862  funcnvuni  5425  fvmptdv2  5767  fsn  5849  fconst2g  5899  funfvima  5918  foco2  5926  isores3  5988  riotaeqimp  6028  eusvobj2  6036  ovmpodv2  6187  ovelrn  6203  f1opw2  6261  suppssov1  6263  suppssfvg  6463  nnmordi  6749  nnmord  6750  qsss  6828  eroveu  6860  th3qlem1  6871  mapsncnv  6930  elixpsn  6970  ixpsnf1o  6971  en1bg  7040  pw2f1odclem  7087  mapxpen  7101  mapunen  7104  en1eqsnbi  7219  updjud  7373  addnidpig  7651  enq0tr  7749  prcdnql  7799  prcunqu  7800  genipv  7824  genpelvl  7827  genpelvu  7828  distrlem5prl  7901  distrlem5pru  7902  aptiprlemu  7955  mulrid  8271  ltne  8358  cnegex  8451  creur  9233  creui  9234  cju  9235  nnsub  9276  un0addcl  9529  un0mulcl  9530  zaddcl  9617  elz2  9649  qmulz  9955  qre  9957  qnegcl  9968  elpqb  9982  xrltne  10146  xlesubadd  10216  iccid  10258  fzsn  10400  fzsuc2  10413  fz1sbc  10430  elfzp12  10433  modqmuladd  10728  bcval5  11125  bcpasc  11128  hashprg  11173  hashfzo  11187  wrdl1s1  11318  cats1un  11413  swrdccat3blem  11431  shftlem  11501  replim  11544  sqrtsq  11729  absle  11774  maxabslemval  11893  negfi  11913  xrmaxiflemval  11935  summodclem2  12068  summodc  12069  zsumdc  12070  fsum3  12073  fsummulc2  12134  fsum00  12148  isumsplit  12177  prodmodclem2  12263  prodmodc  12264  zproddc  12265  fprodseq  12269  prodsnf  12278  fzo0dvdseq  12543  divalgmod  12613  gcdabs1  12685  dvdsgcd  12708  dvdsmulgcd  12721  lcmgcdeq  12780  isprm2lem  12813  dvdsprime  12819  coprm  12841  prmdvdsexpr  12847  rpexp  12850  phibndlem  12913  dfphi2  12917  hashgcdlem  12935  odzdvds  12943  nnoddn2prm  12958  pythagtriplem1  12963  pceulem  12992  pcqmul  13001  pcqcl  13004  pcxnn0cl  13008  pcxcl  13009  pcneg  13023  pcabs  13024  pcgcd1  13026  pcz  13030  pcprmpw2  13031  pcprmpw  13032  dvdsprmpweqle  13035  difsqpwdvds  13036  pcaddlem  13037  pcadd  13038  pcmpt  13041  pockthg  13055  4sqlem2  13087  4sqlem4  13090  mul4sq  13092  mnd1id  13669  0subm  13697  mulgnn0p1  13850  mulgnn0ass  13875  dvreq1  14287  nzrunit  14333  rrgeq0  14410  domneq0  14418  lmodfopnelem2  14473  lss1d  14531  lspsneq0  14574  znidom  14805  znunit  14807  znrrg  14808  istopon  14878  eltg3  14922  tgidm  14939  restbasg  15033  tgrest  15034  tgcn  15073  cnconst  15099  lmss  15111  txbas  15123  txbasval  15132  upxp  15137  blssps  15292  blss  15293  metrest  15371  blssioo  15418  elcncf1di  15444  elply2  15600  plyf  15602  dvdsppwf1o  15857  perfectlem2  15868  perfect  15869  lgsmod  15899  lgsne0  15911  lgsdirnn0  15920  gausslemma2dlem1a  15931  gausslemma2dlem6  15940  lgseisenlem2  15944  lgsquadlem1  15950  lgsquadlem2  15951  2lgslem1b  15962  2sqlem2  15988  mul2sq  15989  2sqlem7  15994  lpvtx  16074  usgredgop  16168  uhgrspansubgrlem  16271  vtxd0nedgbfi  16294  wlk1walkdom  16354  upgrwlkvtxedg  16359  clwwlkext2edg  16417  clwwlknonccat  16428  bj-peano4  16725