Theorem syl5ibcom 155

Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)

Hypotheses

Ref	Expression
imbitrid.1	|- ( ph -> ps )
imbitrid.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5ibcom	|- ( ph -> ( ch -> th ) )

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		imbitrid.1	. . 3 |- ( ph -> ps )
2		imbitrid.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	1, 2	imbitrid 154	. 2 |- ( ch -> ( ph -> th ) )
4	3	com12 30	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimpcd  159  mob2  2952  rmob  3090  preqr1g  3806  issod  4365  sotritrieq  4371  nsuceq0g  4464  suctr  4467  nordeq  4591  suc11g  4604  iss  5004  poirr2  5074  xp11m  5120  tz6.12c  5605  fnbrfvb  5618  fvelimab  5634  foeqcnvco  5858  f1eqcocnv  5859  acexmidlemcase  5938  nna0r  6563  nnawordex  6614  ectocld  6687  ecoptocl  6708  mapsn  6776  eqeng  6856  fopwdom  6932  ordiso  7137  ltexnqq  7520  nsmallnqq  7524  nqprloc  7657  aptiprleml  7751  map2psrprg  7917  0re  8071  lttri3  8151  0cnALT  8261  reapti  8651  recnz  9465  zneo  9473  uzn0  9663  flqidz  10427  ceilqidz  10459  modqid2  10494  modqmuladdnn0  10511  frec2uzrand  10548  frecuzrdgtcl  10555  seq3id  10668  seq3z  10671  facdiv  10881  facwordi  10883  wrdnval  11022  wrdl1s1  11082  maxleb  11498  fsumf1o  11672  dvdsnegb  12090  odd2np1lem  12154  odd2np1  12155  ltoddhalfle  12175  halfleoddlt  12176  opoe  12177  omoe  12178  opeo  12179  omeo  12180  gcddiv  12311  gcdzeq  12314  dvdssqim  12316  lcmgcdeq  12376  coprmdvds2  12386  rpmul  12391  divgcdcoprmex  12395  cncongr2  12397  dvdsprm  12430  coprm  12437  prmdvdsexp  12441  prmdiv  12528  pythagtriplem19  12576  pc2dvds  12624  pcadd  12634  prmpwdvds  12649  exmidunben  12768  intopsn  13170  ismgmid  13180  imasmnd2  13255  isgrpid2  13343  isgrpinv  13357  dfgrp3mlem  13401  imasgrp2  13417  imasrng  13689  imasring  13797  dvdsrcl2  13832  dvdsrtr  13834  dvdsrmul1  13835  lspsneq0  14159  dvdsrzring  14336  znunit  14392  baspartn  14493  bastop  14518  isopn3  14568  lgsdir  15483  lgsne0  15486  lgsquadlem3  15527  bj-peano4  15853  sbthomlem  15926