Theorem syl5ibcom 154

Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)

Hypotheses

Ref	Expression
syl5ib.1	|- ( ph -> ps )
syl5ib.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5ibcom	|- ( ph -> ( ch -> th ) )

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		syl5ib.1	. . 3 |- ( ph -> ps )
2		syl5ib.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	1, 2	syl5ib 153	. 2 |- ( ch -> ( ph -> th ) )
4	3	com12 30	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpcd  158  mob2  2905  rmob  3042  preqr1g  3745  issod  4296  sotritrieq  4302  nsuceq0g  4395  suctr  4398  nordeq  4520  suc11g  4533  iss  4929  poirr2  4995  xp11m  5041  tz6.12c  5515  fnbrfvb  5526  fvelimab  5541  foeqcnvco  5757  f1eqcocnv  5758  acexmidlemcase  5836  nna0r  6442  nnawordex  6492  ectocld  6563  ecoptocl  6584  mapsn  6652  eqeng  6728  fopwdom  6798  ordiso  6997  ltexnqq  7345  nsmallnqq  7349  nqprloc  7482  aptiprleml  7576  map2psrprg  7742  0re  7895  lttri3  7974  0cnALT  8084  reapti  8473  recnz  9280  zneo  9288  uzn0  9477  flqidz  10217  ceilqidz  10247  modqid2  10282  modqmuladdnn0  10299  frec2uzrand  10336  frecuzrdgtcl  10343  seq3id  10439  seq3z  10442  facdiv  10647  facwordi  10649  maxleb  11154  fsumf1o  11327  dvdsnegb  11744  odd2np1lem  11805  odd2np1  11806  ltoddhalfle  11826  halfleoddlt  11827  opoe  11828  omoe  11829  opeo  11830  omeo  11831  gcddiv  11948  gcdzeq  11951  dvdssqim  11953  lcmgcdeq  12011  coprmdvds2  12021  rpmul  12026  divgcdcoprmex  12030  cncongr2  12032  dvdsprm  12065  coprm  12072  prmdvdsexp  12076  prmdiv  12163  pythagtriplem19  12210  pc2dvds  12257  pcadd  12267  prmpwdvds  12281  exmidunben  12355  baspartn  12648  bastop  12675  isopn3  12725  lgsdir  13536  lgsne0  13539  bj-peano4  13797  sbthomlem  13864