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  2986  rmob  3125  preqr1g  3849  issod  4416  sotritrieq  4422  nsuceq0g  4515  suctr  4518  nordeq  4642  suc11g  4655  iss  5059  poirr2  5129  xp11m  5175  tz6.12c  5669  fnbrfvb  5684  fvelimab  5702  foeqcnvco  5930  f1eqcocnv  5931  acexmidlemcase  6012  nna0r  6645  nnawordex  6696  ectocld  6769  ecoptocl  6790  mapsn  6858  eqeng  6938  fopwdom  7021  ordiso  7234  ltexnqq  7627  nsmallnqq  7631  nqprloc  7764  aptiprleml  7858  map2psrprg  8024  0re  8178  lttri3  8258  0cnALT  8368  reapti  8758  recnz  9572  zneo  9580  uzn0  9771  flqidz  10545  ceilqidz  10577  modqid2  10612  modqmuladdnn0  10629  frec2uzrand  10666  frecuzrdgtcl  10673  seq3id  10786  seq3z  10789  facdiv  10999  facwordi  11001  wrdnval  11143  wrdl1s1  11206  maxleb  11776  fsumf1o  11950  dvdsnegb  12368  odd2np1lem  12432  odd2np1  12433  ltoddhalfle  12453  halfleoddlt  12454  opoe  12455  omoe  12456  opeo  12457  omeo  12458  gcddiv  12589  gcdzeq  12592  dvdssqim  12594  lcmgcdeq  12654  coprmdvds2  12664  rpmul  12669  divgcdcoprmex  12673  cncongr2  12675  dvdsprm  12708  coprm  12715  prmdvdsexp  12719  prmdiv  12806  pythagtriplem19  12854  pc2dvds  12902  pcadd  12912  prmpwdvds  12927  exmidunben  13046  intopsn  13449  ismgmid  13459  imasmnd2  13534  isgrpid2  13622  isgrpinv  13636  dfgrp3mlem  13680  imasgrp2  13696  imasrng  13968  imasring  14076  dvdsrcl2  14112  dvdsrtr  14114  dvdsrmul1  14115  lspsneq0  14439  dvdsrzring  14616  znunit  14672  baspartn  14773  bastop  14798  isopn3  14848  lgsdir  15763  lgsne0  15766  lgsquadlem3  15807  uhgrm  15928  upgrfnen  15948  umgrfnen  15958  eupth2lem2dc  16309  bj-peano4  16550  sbthomlem  16629