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  11742  fsumf1o  11916  dvdsnegb  12334  odd2np1lem  12398  odd2np1  12399  ltoddhalfle  12419  halfleoddlt  12420  opoe  12421  omoe  12422  opeo  12423  omeo  12424  gcddiv  12555  gcdzeq  12558  dvdssqim  12560  lcmgcdeq  12620  coprmdvds2  12630  rpmul  12635  divgcdcoprmex  12639  cncongr2  12641  dvdsprm  12674  coprm  12681  prmdvdsexp  12685  prmdiv  12772  pythagtriplem19  12820  pc2dvds  12868  pcadd  12878  prmpwdvds  12893  exmidunben  13012  intopsn  13415  ismgmid  13425  imasmnd2  13500  isgrpid2  13588  isgrpinv  13602  dfgrp3mlem  13646  imasgrp2  13662  imasrng  13934  imasring  14042  dvdsrcl2  14078  dvdsrtr  14080  dvdsrmul1  14081  lspsneq0  14405  dvdsrzring  14582  znunit  14638  baspartn  14739  bastop  14764  isopn3  14814  lgsdir  15729  lgsne0  15732  lgsquadlem3  15773  uhgrm  15893  upgrfnen  15913  umgrfnen  15923  bj-peano4  16373  sbthomlem  16453