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  2918  rmob  3056  preqr1g  3767  issod  4320  sotritrieq  4326  nsuceq0g  4419  suctr  4422  nordeq  4544  suc11g  4557  iss  4954  poirr2  5022  xp11m  5068  tz6.12c  5546  fnbrfvb  5557  fvelimab  5573  foeqcnvco  5791  f1eqcocnv  5792  acexmidlemcase  5870  nna0r  6479  nnawordex  6530  ectocld  6601  ecoptocl  6622  mapsn  6690  eqeng  6766  fopwdom  6836  ordiso  7035  ltexnqq  7407  nsmallnqq  7411  nqprloc  7544  aptiprleml  7638  map2psrprg  7804  0re  7957  lttri3  8037  0cnALT  8147  reapti  8536  recnz  9346  zneo  9354  uzn0  9543  flqidz  10286  ceilqidz  10316  modqid2  10351  modqmuladdnn0  10368  frec2uzrand  10405  frecuzrdgtcl  10412  seq3id  10508  seq3z  10511  facdiv  10718  facwordi  10720  maxleb  11225  fsumf1o  11398  dvdsnegb  11815  odd2np1lem  11877  odd2np1  11878  ltoddhalfle  11898  halfleoddlt  11899  opoe  11900  omoe  11901  opeo  11902  omeo  11903  gcddiv  12020  gcdzeq  12023  dvdssqim  12025  lcmgcdeq  12083  coprmdvds2  12093  rpmul  12098  divgcdcoprmex  12102  cncongr2  12104  dvdsprm  12137  coprm  12144  prmdvdsexp  12148  prmdiv  12235  pythagtriplem19  12282  pc2dvds  12329  pcadd  12339  prmpwdvds  12353  exmidunben  12427  intopsn  12786  ismgmid  12796  isgrpid2  12913  isgrpinv  12926  dfgrp3mlem  12968  dvdsrcl2  13268  dvdsrtr  13270  dvdsrmul1  13271  dvdsrzring  13496  baspartn  13553  bastop  13578  isopn3  13628  lgsdir  14439  lgsne0  14442  bj-peano4  14710  sbthomlem  14776