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  2941  rmob  3079  preqr1g  3793  issod  4351  sotritrieq  4357  nsuceq0g  4450  suctr  4453  nordeq  4577  suc11g  4590  iss  4989  poirr2  5059  xp11m  5105  tz6.12c  5585  fnbrfvb  5598  fvelimab  5614  foeqcnvco  5834  f1eqcocnv  5835  acexmidlemcase  5914  nna0r  6533  nnawordex  6584  ectocld  6657  ecoptocl  6678  mapsn  6746  eqeng  6822  fopwdom  6894  ordiso  7097  ltexnqq  7470  nsmallnqq  7474  nqprloc  7607  aptiprleml  7701  map2psrprg  7867  0re  8021  lttri3  8101  0cnALT  8211  reapti  8600  recnz  9413  zneo  9421  uzn0  9611  flqidz  10358  ceilqidz  10390  modqid2  10425  modqmuladdnn0  10442  frec2uzrand  10479  frecuzrdgtcl  10486  seq3id  10599  seq3z  10602  facdiv  10812  facwordi  10814  wrdnval  10947  maxleb  11363  fsumf1o  11536  dvdsnegb  11954  odd2np1lem  12016  odd2np1  12017  ltoddhalfle  12037  halfleoddlt  12038  opoe  12039  omoe  12040  opeo  12041  omeo  12042  gcddiv  12159  gcdzeq  12162  dvdssqim  12164  lcmgcdeq  12224  coprmdvds2  12234  rpmul  12239  divgcdcoprmex  12243  cncongr2  12245  dvdsprm  12278  coprm  12285  prmdvdsexp  12289  prmdiv  12376  pythagtriplem19  12423  pc2dvds  12471  pcadd  12481  prmpwdvds  12496  exmidunben  12586  intopsn  12953  ismgmid  12963  isgrpid2  13115  isgrpinv  13129  dfgrp3mlem  13173  imasgrp2  13183  imasrng  13455  imasring  13563  dvdsrcl2  13598  dvdsrtr  13600  dvdsrmul1  13601  lspsneq0  13925  dvdsrzring  14102  znunit  14158  baspartn  14229  bastop  14254  isopn3  14304  lgsdir  15192  lgsne0  15195  lgsquadlem3  15236  bj-peano4  15517  sbthomlem  15585