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  2997  rmob  3136  preqr1g  3870  issod  4440  sotritrieq  4446  nsuceq0g  4539  suctr  4542  nordeq  4666  suc11g  4679  iss  5084  poirr2  5155  xp11m  5201  tz6.12c  5700  fnbrfvb  5715  fvelimab  5733  foeqcnvco  5963  f1eqcocnv  5964  acexmidlemcase  6045  nna0r  6711  nnawordex  6762  ectocld  6835  ecoptocl  6856  mapsnd  6923  mapsn  6925  eqeng  7005  fopwdom  7089  ordiso  7327  ltexnqq  7723  nsmallnqq  7727  nqprloc  7860  aptiprleml  7954  map2psrprg  8120  0re  8274  lttri3  8353  0cnALT  8463  reapti  8853  recnz  9671  zneo  9679  uzn0  9870  flqidz  10646  ceilqidz  10678  modqid2  10713  modqmuladdnn0  10730  frec2uzrand  10767  frecuzrdgtcl  10774  seq3id  10887  seq3z  10890  facdiv  11100  facwordi  11102  wrdnval  11255  wrdl1s1  11318  maxleb  11901  fsumf1o  12076  dvdsnegb  12494  odd2np1lem  12558  odd2np1  12559  ltoddhalfle  12579  halfleoddlt  12580  opoe  12581  omoe  12582  opeo  12583  omeo  12584  gcddiv  12715  gcdzeq  12718  dvdssqim  12720  lcmgcdeq  12780  coprmdvds2  12790  rpmul  12795  divgcdcoprmex  12799  cncongr2  12801  dvdsprm  12834  coprm  12841  prmdvdsexp  12845  prmdiv  12932  pythagtriplem19  12980  pc2dvds  13028  pcadd  13038  prmpwdvds  13053  exmidunben  13177  intopsn  13580  ismgmid  13590  imasmnd2  13665  isgrpid2  13753  isgrpinv  13767  dfgrp3mlem  13811  imasgrp2  13827  imasrng  14100  imasring  14208  dvdsrcl2  14244  dvdsrtr  14246  dvdsrmul1  14247  lspsneq0  14574  dvdsrzring  14751  znunit  14807  baspartn  14915  bastop  14940  isopn3  14990  pellexlem1  15845  lgsdir  15908  lgsne0  15911  lgsquadlem3  15952  uhgrm  16073  upgrfnen  16093  umgrfnen  16103  eupth2lem2dc  16454  eupth2lem3lem6fi  16466  bj-peano4  16725  sbthomlem  16805