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  2987  rmob  3126  preqr1g  3854  issod  4422  sotritrieq  4428  nsuceq0g  4521  suctr  4524  nordeq  4648  suc11g  4661  iss  5065  poirr2  5136  xp11m  5182  tz6.12c  5678  fnbrfvb  5693  fvelimab  5711  foeqcnvco  5941  f1eqcocnv  5942  acexmidlemcase  6023  nna0r  6689  nnawordex  6740  ectocld  6813  ecoptocl  6834  mapsn  6902  eqeng  6982  fopwdom  7065  ordiso  7278  ltexnqq  7671  nsmallnqq  7675  nqprloc  7808  aptiprleml  7902  map2psrprg  8068  0re  8222  lttri3  8301  0cnALT  8411  reapti  8801  recnz  9617  zneo  9625  uzn0  9816  flqidz  10592  ceilqidz  10624  modqid2  10659  modqmuladdnn0  10676  frec2uzrand  10713  frecuzrdgtcl  10720  seq3id  10833  seq3z  10836  facdiv  11046  facwordi  11048  wrdnval  11193  wrdl1s1  11256  maxleb  11839  fsumf1o  12014  dvdsnegb  12432  odd2np1lem  12496  odd2np1  12497  ltoddhalfle  12517  halfleoddlt  12518  opoe  12519  omoe  12520  opeo  12521  omeo  12522  gcddiv  12653  gcdzeq  12656  dvdssqim  12658  lcmgcdeq  12718  coprmdvds2  12728  rpmul  12733  divgcdcoprmex  12737  cncongr2  12739  dvdsprm  12772  coprm  12779  prmdvdsexp  12783  prmdiv  12870  pythagtriplem19  12918  pc2dvds  12966  pcadd  12976  prmpwdvds  12991  exmidunben  13110  intopsn  13513  ismgmid  13523  imasmnd2  13598  isgrpid2  13686  isgrpinv  13700  dfgrp3mlem  13744  imasgrp2  13760  imasrng  14033  imasring  14141  dvdsrcl2  14177  dvdsrtr  14179  dvdsrmul1  14180  lspsneq0  14505  dvdsrzring  14682  znunit  14738  baspartn  14844  bastop  14869  isopn3  14919  pellexlem1  15774  lgsdir  15837  lgsne0  15840  lgsquadlem3  15881  uhgrm  16002  upgrfnen  16022  umgrfnen  16032  eupth2lem2dc  16383  eupth2lem3lem6fi  16395  bj-peano4  16654  sbthomlem  16736