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  2983  rmob  3122  preqr1g  3843  issod  4409  sotritrieq  4415  nsuceq0g  4508  suctr  4511  nordeq  4635  suc11g  4648  iss  5050  poirr2  5120  xp11m  5166  tz6.12c  5656  fnbrfvb  5671  fvelimab  5689  foeqcnvco  5913  f1eqcocnv  5914  acexmidlemcase  5995  nna0r  6622  nnawordex  6673  ectocld  6746  ecoptocl  6767  mapsn  6835  eqeng  6915  fopwdom  6993  ordiso  7199  ltexnqq  7591  nsmallnqq  7595  nqprloc  7728  aptiprleml  7822  map2psrprg  7988  0re  8142  lttri3  8222  0cnALT  8332  reapti  8722  recnz  9536  zneo  9544  uzn0  9734  flqidz  10501  ceilqidz  10533  modqid2  10568  modqmuladdnn0  10585  frec2uzrand  10622  frecuzrdgtcl  10629  seq3id  10742  seq3z  10745  facdiv  10955  facwordi  10957  wrdnval  11097  wrdl1s1  11158  maxleb  11722  fsumf1o  11896  dvdsnegb  12314  odd2np1lem  12378  odd2np1  12379  ltoddhalfle  12399  halfleoddlt  12400  opoe  12401  omoe  12402  opeo  12403  omeo  12404  gcddiv  12535  gcdzeq  12538  dvdssqim  12540  lcmgcdeq  12600  coprmdvds2  12610  rpmul  12615  divgcdcoprmex  12619  cncongr2  12621  dvdsprm  12654  coprm  12661  prmdvdsexp  12665  prmdiv  12752  pythagtriplem19  12800  pc2dvds  12848  pcadd  12858  prmpwdvds  12873  exmidunben  12992  intopsn  13395  ismgmid  13405  imasmnd2  13480  isgrpid2  13568  isgrpinv  13582  dfgrp3mlem  13626  imasgrp2  13642  imasrng  13914  imasring  14022  dvdsrcl2  14057  dvdsrtr  14059  dvdsrmul1  14060  lspsneq0  14384  dvdsrzring  14561  znunit  14617  baspartn  14718  bastop  14743  isopn3  14793  lgsdir  15708  lgsne0  15711  lgsquadlem3  15752  uhgrm  15872  upgrfnen  15892  umgrfnen  15902  bj-peano4  16276  sbthomlem  16352