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  2944  rmob  3082  preqr1g  3797  issod  4355  sotritrieq  4361  nsuceq0g  4454  suctr  4457  nordeq  4581  suc11g  4594  iss  4993  poirr2  5063  xp11m  5109  tz6.12c  5591  fnbrfvb  5604  fvelimab  5620  foeqcnvco  5840  f1eqcocnv  5841  acexmidlemcase  5920  nna0r  6545  nnawordex  6596  ectocld  6669  ecoptocl  6690  mapsn  6758  eqeng  6834  fopwdom  6906  ordiso  7111  ltexnqq  7494  nsmallnqq  7498  nqprloc  7631  aptiprleml  7725  map2psrprg  7891  0re  8045  lttri3  8125  0cnALT  8235  reapti  8625  recnz  9438  zneo  9446  uzn0  9636  flqidz  10395  ceilqidz  10427  modqid2  10462  modqmuladdnn0  10479  frec2uzrand  10516  frecuzrdgtcl  10523  seq3id  10636  seq3z  10639  facdiv  10849  facwordi  10851  wrdnval  10984  maxleb  11400  fsumf1o  11574  dvdsnegb  11992  odd2np1lem  12056  odd2np1  12057  ltoddhalfle  12077  halfleoddlt  12078  opoe  12079  omoe  12080  opeo  12081  omeo  12082  gcddiv  12213  gcdzeq  12216  dvdssqim  12218  lcmgcdeq  12278  coprmdvds2  12288  rpmul  12293  divgcdcoprmex  12297  cncongr2  12299  dvdsprm  12332  coprm  12339  prmdvdsexp  12343  prmdiv  12430  pythagtriplem19  12478  pc2dvds  12526  pcadd  12536  prmpwdvds  12551  exmidunben  12670  intopsn  13071  ismgmid  13081  imasmnd2  13156  isgrpid2  13244  isgrpinv  13258  dfgrp3mlem  13302  imasgrp2  13318  imasrng  13590  imasring  13698  dvdsrcl2  13733  dvdsrtr  13735  dvdsrmul1  13736  lspsneq0  14060  dvdsrzring  14237  znunit  14293  baspartn  14394  bastop  14419  isopn3  14469  lgsdir  15384  lgsne0  15387  lgsquadlem3  15428  bj-peano4  15709  sbthomlem  15782