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  2984  rmob  3123  preqr1g  3847  issod  4414  sotritrieq  4420  nsuceq0g  4513  suctr  4516  nordeq  4640  suc11g  4653  iss  5057  poirr2  5127  xp11m  5173  tz6.12c  5665  fnbrfvb  5680  fvelimab  5698  foeqcnvco  5926  f1eqcocnv  5927  acexmidlemcase  6008  nna0r  6641  nnawordex  6692  ectocld  6765  ecoptocl  6786  mapsn  6854  eqeng  6934  fopwdom  7017  ordiso  7226  ltexnqq  7618  nsmallnqq  7622  nqprloc  7755  aptiprleml  7849  map2psrprg  8015  0re  8169  lttri3  8249  0cnALT  8359  reapti  8749  recnz  9563  zneo  9571  uzn0  9762  flqidz  10536  ceilqidz  10568  modqid2  10603  modqmuladdnn0  10620  frec2uzrand  10657  frecuzrdgtcl  10664  seq3id  10777  seq3z  10780  facdiv  10990  facwordi  10992  wrdnval  11134  wrdl1s1  11197  maxleb  11767  fsumf1o  11941  dvdsnegb  12359  odd2np1lem  12423  odd2np1  12424  ltoddhalfle  12444  halfleoddlt  12445  opoe  12446  omoe  12447  opeo  12448  omeo  12449  gcddiv  12580  gcdzeq  12583  dvdssqim  12585  lcmgcdeq  12645  coprmdvds2  12655  rpmul  12660  divgcdcoprmex  12664  cncongr2  12666  dvdsprm  12699  coprm  12706  prmdvdsexp  12710  prmdiv  12797  pythagtriplem19  12845  pc2dvds  12893  pcadd  12903  prmpwdvds  12918  exmidunben  13037  intopsn  13440  ismgmid  13450  imasmnd2  13525  isgrpid2  13613  isgrpinv  13627  dfgrp3mlem  13671  imasgrp2  13687  imasrng  13959  imasring  14067  dvdsrcl2  14103  dvdsrtr  14105  dvdsrmul1  14106  lspsneq0  14430  dvdsrzring  14607  znunit  14663  baspartn  14764  bastop  14789  isopn3  14839  lgsdir  15754  lgsne0  15757  lgsquadlem3  15798  uhgrm  15919  upgrfnen  15939  umgrfnen  15949  bj-peano4  16486  sbthomlem  16565