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  2864  rmob  3001  preqr1g  3693  issod  4241  sotritrieq  4247  nsuceq0g  4340  suctr  4343  nordeq  4459  suc11g  4472  iss  4865  poirr2  4931  xp11m  4977  tz6.12c  5451  fnbrfvb  5462  fvelimab  5477  foeqcnvco  5691  f1eqcocnv  5692  acexmidlemcase  5769  nna0r  6374  nnawordex  6424  ectocld  6495  ecoptocl  6516  mapsn  6584  eqeng  6660  fopwdom  6730  ordiso  6921  ltexnqq  7216  nsmallnqq  7220  nqprloc  7353  aptiprleml  7447  map2psrprg  7613  0re  7766  lttri3  7844  0cnALT  7952  reapti  8341  recnz  9144  zneo  9152  uzn0  9341  flqidz  10059  ceilqidz  10089  modqid2  10124  modqmuladdnn0  10141  frec2uzrand  10178  frecuzrdgtcl  10185  seq3id  10281  seq3z  10284  facdiv  10484  facwordi  10486  maxleb  10988  fsumf1o  11159  dvdsnegb  11510  odd2np1lem  11569  odd2np1  11570  ltoddhalfle  11590  halfleoddlt  11591  opoe  11592  omoe  11593  opeo  11594  omeo  11595  gcddiv  11707  gcdzeq  11710  dvdssqim  11712  lcmgcdeq  11764  coprmdvds2  11774  rpmul  11779  divgcdcoprmex  11783  cncongr2  11785  dvdsprm  11817  coprm  11822  prmdvdsexp  11826  exmidunben  11939  baspartn  12217  bastop  12244  isopn3  12294  bj-peano4  13153  sbthomlem  13220