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  2953  rmob  3091  preqr1g  3807  issod  4366  sotritrieq  4372  nsuceq0g  4465  suctr  4468  nordeq  4592  suc11g  4605  iss  5005  poirr2  5075  xp11m  5121  tz6.12c  5606  fnbrfvb  5619  fvelimab  5635  foeqcnvco  5859  f1eqcocnv  5860  acexmidlemcase  5939  nna0r  6564  nnawordex  6615  ectocld  6688  ecoptocl  6709  mapsn  6777  eqeng  6857  fopwdom  6933  ordiso  7138  ltexnqq  7521  nsmallnqq  7525  nqprloc  7658  aptiprleml  7752  map2psrprg  7918  0re  8072  lttri3  8152  0cnALT  8262  reapti  8652  recnz  9466  zneo  9474  uzn0  9664  flqidz  10429  ceilqidz  10461  modqid2  10496  modqmuladdnn0  10513  frec2uzrand  10550  frecuzrdgtcl  10557  seq3id  10670  seq3z  10673  facdiv  10883  facwordi  10885  wrdnval  11024  wrdl1s1  11084  maxleb  11527  fsumf1o  11701  dvdsnegb  12119  odd2np1lem  12183  odd2np1  12184  ltoddhalfle  12204  halfleoddlt  12205  opoe  12206  omoe  12207  opeo  12208  omeo  12209  gcddiv  12340  gcdzeq  12343  dvdssqim  12345  lcmgcdeq  12405  coprmdvds2  12415  rpmul  12420  divgcdcoprmex  12424  cncongr2  12426  dvdsprm  12459  coprm  12466  prmdvdsexp  12470  prmdiv  12557  pythagtriplem19  12605  pc2dvds  12653  pcadd  12663  prmpwdvds  12678  exmidunben  12797  intopsn  13199  ismgmid  13209  imasmnd2  13284  isgrpid2  13372  isgrpinv  13386  dfgrp3mlem  13430  imasgrp2  13446  imasrng  13718  imasring  13826  dvdsrcl2  13861  dvdsrtr  13863  dvdsrmul1  13864  lspsneq0  14188  dvdsrzring  14365  znunit  14421  baspartn  14522  bastop  14547  isopn3  14597  lgsdir  15512  lgsne0  15515  lgsquadlem3  15556  bj-peano4  15891  sbthomlem  15964