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  5931  f1eqcocnv  5932  acexmidlemcase  6013  nna0r  6646  nnawordex  6697  ectocld  6770  ecoptocl  6791  mapsn  6859  eqeng  6939  fopwdom  7022  ordiso  7235  ltexnqq  7628  nsmallnqq  7632  nqprloc  7765  aptiprleml  7859  map2psrprg  8025  0re  8179  lttri3  8259  0cnALT  8369  reapti  8759  recnz  9573  zneo  9581  uzn0  9772  flqidz  10547  ceilqidz  10579  modqid2  10614  modqmuladdnn0  10631  frec2uzrand  10668  frecuzrdgtcl  10675  seq3id  10788  seq3z  10791  facdiv  11001  facwordi  11003  wrdnval  11148  wrdl1s1  11211  maxleb  11794  fsumf1o  11969  dvdsnegb  12387  odd2np1lem  12451  odd2np1  12452  ltoddhalfle  12472  halfleoddlt  12473  opoe  12474  omoe  12475  opeo  12476  omeo  12477  gcddiv  12608  gcdzeq  12611  dvdssqim  12613  lcmgcdeq  12673  coprmdvds2  12683  rpmul  12688  divgcdcoprmex  12692  cncongr2  12694  dvdsprm  12727  coprm  12734  prmdvdsexp  12738  prmdiv  12825  pythagtriplem19  12873  pc2dvds  12921  pcadd  12931  prmpwdvds  12946  exmidunben  13065  intopsn  13468  ismgmid  13478  imasmnd2  13553  isgrpid2  13641  isgrpinv  13655  dfgrp3mlem  13699  imasgrp2  13715  imasrng  13988  imasring  14096  dvdsrcl2  14132  dvdsrtr  14134  dvdsrmul1  14135  lspsneq0  14459  dvdsrzring  14636  znunit  14692  baspartn  14793  bastop  14818  isopn3  14868  lgsdir  15783  lgsne0  15786  lgsquadlem3  15827  uhgrm  15948  upgrfnen  15968  umgrfnen  15978  eupth2lem2dc  16329  eupth2lem3lem6fi  16341  bj-peano4  16601  sbthomlem  16680