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  3006  rmob  3145  preqr1g  3886  issod  4459  sotritrieq  4465  nsuceq0g  4558  suctr  4561  nordeq  4686  suc11g  4699  iss  5104  poirr2  5175  xp11m  5221  tz6.12c  5720  fnbrfvb  5735  fvelimab  5753  foeqcnvco  5986  f1eqcocnv  5987  acexmidlemcase  6070  nna0r  6741  nnawordex  6792  ectocld  6865  ecoptocl  6886  mapsnd  6960  mapsn  6962  eqeng  7042  fopwdom  7126  ordiso  7366  ltexnqq  7765  nsmallnqq  7769  nqprloc  7902  aptiprleml  7996  map2psrprg  8162  0re  8316  lttri3  8395  0cnALT  8506  reapti  8897  recnz  9718  zneo  9726  uzn0  9917  flqidz  10699  ceilqidz  10731  modqid2  10766  modqmuladdnn0  10783  frec2uzrand  10820  frecuzrdgtcl  10827  seq3id  10940  seq3z  10943  facdiv  11154  facwordi  11156  wrdnval  11313  wrdl1s1  11376  maxleb  11960  fsumf1o  12135  dvdsnegb  12553  odd2np1lem  12617  odd2np1  12618  ltoddhalfle  12638  halfleoddlt  12639  opoe  12640  omoe  12641  opeo  12642  omeo  12643  gcddiv  12774  gcdzeq  12777  dvdssqim  12779  lcmgcdeq  12839  coprmdvds2  12849  rpmul  12854  divgcdcoprmex  12858  cncongr2  12860  dvdsprm  12893  coprm  12900  prmdvdsexp  12904  prmdiv  12991  pythagtriplem19  13039  pc2dvds  13087  pcadd  13097  prmpwdvds  13112  exmidunben  13295  intopsn  13664  ismgmid  13674  imasmnd2  13736  isgrpid2  13822  isgrpinv  13836  dfgrp3mlem  13880  imasgrp2  13890  imasrng  14230  imasring  14342  dvdsrcl2  14379  dvdsrtr  14381  dvdsrmul1  14382  lspsneq0  14735  dvdsrzring  14910  znunit  14966  baspartn  15074  bastop  15099  isopn3  15149  pellexlem1  16005  lgsdir  16068  lgsne0  16071  lgsquadlem3  16112  uhgrm  16233  upgrfnen  16253  umgrfnen  16263  eupth2lem2dc  16614  eupth2lem3lem6fi  16626  bj-peano4  16895  sbthomlem  16975