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  2983  rmob  3122  preqr1g  3844  issod  4410  sotritrieq  4416  nsuceq0g  4509  suctr  4512  nordeq  4636  suc11g  4649  iss  5051  poirr2  5121  xp11m  5167  tz6.12c  5659  fnbrfvb  5674  fvelimab  5692  foeqcnvco  5920  f1eqcocnv  5921  acexmidlemcase  6002  nna0r  6632  nnawordex  6683  ectocld  6756  ecoptocl  6777  mapsn  6845  eqeng  6925  fopwdom  7005  ordiso  7214  ltexnqq  7606  nsmallnqq  7610  nqprloc  7743  aptiprleml  7837  map2psrprg  8003  0re  8157  lttri3  8237  0cnALT  8347  reapti  8737  recnz  9551  zneo  9559  uzn0  9750  flqidz  10518  ceilqidz  10550  modqid2  10585  modqmuladdnn0  10602  frec2uzrand  10639  frecuzrdgtcl  10646  seq3id  10759  seq3z  10762  facdiv  10972  facwordi  10974  wrdnval  11115  wrdl1s1  11178  maxleb  11743  fsumf1o  11917  dvdsnegb  12335  odd2np1lem  12399  odd2np1  12400  ltoddhalfle  12420  halfleoddlt  12421  opoe  12422  omoe  12423  opeo  12424  omeo  12425  gcddiv  12556  gcdzeq  12559  dvdssqim  12561  lcmgcdeq  12621  coprmdvds2  12631  rpmul  12636  divgcdcoprmex  12640  cncongr2  12642  dvdsprm  12675  coprm  12682  prmdvdsexp  12686  prmdiv  12773  pythagtriplem19  12821  pc2dvds  12869  pcadd  12879  prmpwdvds  12894  exmidunben  13013  intopsn  13416  ismgmid  13426  imasmnd2  13501  isgrpid2  13589  isgrpinv  13603  dfgrp3mlem  13647  imasgrp2  13663  imasrng  13935  imasring  14043  dvdsrcl2  14079  dvdsrtr  14081  dvdsrmul1  14082  lspsneq0  14406  dvdsrzring  14583  znunit  14639  baspartn  14740  bastop  14765  isopn3  14815  lgsdir  15730  lgsne0  15733  lgsquadlem3  15774  uhgrm  15894  upgrfnen  15914  umgrfnen  15924  bj-peano4  16401  sbthomlem  16481