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  3000  rmob  3139  preqr1g  3875  issod  4445  sotritrieq  4451  nsuceq0g  4544  suctr  4547  nordeq  4671  suc11g  4684  iss  5089  poirr2  5160  xp11m  5206  tz6.12c  5705  fnbrfvb  5720  fvelimab  5738  foeqcnvco  5969  f1eqcocnv  5970  acexmidlemcase  6053  nna0r  6724  nnawordex  6775  ectocld  6848  ecoptocl  6869  mapsnd  6936  mapsn  6938  eqeng  7018  fopwdom  7102  ordiso  7340  ltexnqq  7739  nsmallnqq  7743  nqprloc  7876  aptiprleml  7970  map2psrprg  8136  0re  8290  lttri3  8369  0cnALT  8479  reapti  8870  recnz  9689  zneo  9697  uzn0  9888  flqidz  10670  ceilqidz  10702  modqid2  10737  modqmuladdnn0  10754  frec2uzrand  10791  frecuzrdgtcl  10798  seq3id  10911  seq3z  10914  facdiv  11125  facwordi  11127  wrdnval  11280  wrdl1s1  11343  maxleb  11926  fsumf1o  12101  dvdsnegb  12519  odd2np1lem  12583  odd2np1  12584  ltoddhalfle  12604  halfleoddlt  12605  opoe  12606  omoe  12607  opeo  12608  omeo  12609  gcddiv  12740  gcdzeq  12743  dvdssqim  12745  lcmgcdeq  12805  coprmdvds2  12815  rpmul  12820  divgcdcoprmex  12824  cncongr2  12826  dvdsprm  12859  coprm  12866  prmdvdsexp  12870  prmdiv  12957  pythagtriplem19  13005  pc2dvds  13053  pcadd  13063  prmpwdvds  13078  exmidunben  13261  intopsn  13630  ismgmid  13640  imasmnd2  13707  isgrpid2  13795  isgrpinv  13809  dfgrp3mlem  13853  imasgrp2  13863  imasrng  14195  imasring  14307  dvdsrcl2  14344  dvdsrtr  14346  dvdsrmul1  14347  lspsneq0  14700  dvdsrzring  14877  znunit  14933  baspartn  15041  bastop  15066  isopn3  15116  pellexlem1  15971  lgsdir  16034  lgsne0  16037  lgsquadlem3  16078  uhgrm  16199  upgrfnen  16219  umgrfnen  16229  eupth2lem2dc  16580  eupth2lem3lem6fi  16592  bj-peano4  16851  sbthomlem  16931