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  2888  rmob  3025  preqr1g  3725  issod  4274  sotritrieq  4280  nsuceq0g  4373  suctr  4376  nordeq  4497  suc11g  4510  iss  4905  poirr2  4971  xp11m  5017  tz6.12c  5491  fnbrfvb  5502  fvelimab  5517  foeqcnvco  5731  f1eqcocnv  5732  acexmidlemcase  5809  nna0r  6414  nnawordex  6464  ectocld  6535  ecoptocl  6556  mapsn  6624  eqeng  6700  fopwdom  6770  ordiso  6966  ltexnqq  7307  nsmallnqq  7311  nqprloc  7444  aptiprleml  7538  map2psrprg  7704  0re  7857  lttri3  7936  0cnALT  8044  reapti  8433  recnz  9236  zneo  9244  uzn0  9433  flqidz  10163  ceilqidz  10193  modqid2  10228  modqmuladdnn0  10245  frec2uzrand  10282  frecuzrdgtcl  10289  seq3id  10385  seq3z  10388  facdiv  10589  facwordi  10591  maxleb  11093  fsumf1o  11264  dvdsnegb  11677  odd2np1lem  11736  odd2np1  11737  ltoddhalfle  11757  halfleoddlt  11758  opoe  11759  omoe  11760  opeo  11761  omeo  11762  gcddiv  11875  gcdzeq  11878  dvdssqim  11880  lcmgcdeq  11932  coprmdvds2  11942  rpmul  11947  divgcdcoprmex  11951  cncongr2  11953  dvdsprm  11985  coprm  11990  prmdvdsexp  11994  exmidunben  12114  baspartn  12395  bastop  12422  isopn3  12472  bj-peano4  13476  sbthomlem  13545