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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimpcd  159  mob2  3006  rmob  3145  preqr1g  3891  issod  4464  sotritrieq  4470  nsuceq0g  4563  suctr  4566  nordeq  4691  suc11g  4704  iss  5109  poirr2  5180  xp11m  5226  tz6.12c  5725  fnbrfvb  5741  fvelimab  5759  foeqcnvco  5996  f1eqcocnv  5997  acexmidlemcase  6080  nna0r  6751  nnawordex  6802  ectocld  6875  ecoptocl  6896  mapsnd  6970  mapsn  6972  eqeng  7052  fopwdom  7136  ordiso  7377  ltexnqq  7776  nsmallnqq  7780  nqprloc  7913  aptiprleml  8007  map2psrprg  8173  0re  8327  lttri3  8406  0cnALT  8518  reapti  8910  recnz  9744  zneo  9752  uzn0  9948  flqidz  10736  ceilqidz  10768  modqid2  10803  modqmuladdnn0  10820  frec2uzrand  10857  frecuzrdgtcl  10864  seq3id  10977  seq3z  10980  facdiv  11192  facwordi  11194  wrdnval  11351  wrdl1s1  11414  maxleb  11999  fsumf1o  12176  dvdsnegb  12594  odd2np1lem  12658  odd2np1  12659  ltoddhalfle  12679  halfleoddlt  12680  opoe  12681  omoe  12682  opeo  12683  omeo  12684  gcddiv  12815  gcdzeq  12818  dvdssqim  12820  lcmgcdeq  12880  coprmdvds2  12890  rpmul  12895  divgcdcoprmex  12899  cncongr2  12901  dvdsprm  12935  coprm  12942  prmdvdsexp  12946  prmdiv  13036  pythagtriplem19  13084  pc2dvds  13132  pcadd  13142  prmpwdvds  13157  exmidunben  13369  intopsn  13740  ismgmid  13750  imasmnd2  13812  isgrpid2  13898  isgrpinv  13912  dfgrp3mlem  13956  imasgrp2  13966  imasrng  14339  imasring  14453  dvdsrcl2  14490  dvdsrtr  14492  dvdsrmul1  14493  lspsneq0  14847  dvdsrzring  15022  znunit  15078  baspartn  15242  bastop  15267  isopn3  15317  pellexlem1  16190  ppiublem1  16252  lgsdir  16320  lgsne0  16323  lgsquadlem3  16364  uhgrm  16485  upgrfnen  16505  umgrfnen  16515  eupth2lem2dc  16866  eupth2lem3lem6fi  16878  bj-peano4  17147  sbthomlem  17236