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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimpcd  159  mob2  3006  rmob  3145  preqr1g  3891  issod  4464  sotritrieq  4470  nsuceq0g  4563  suctr  4566  nordeq  4691  suc11g  4704  iss  5109  poirr2  5180  xp11m  5226  tz6.12c  5725  fnbrfvb  5741  fvelimab  5759  foeqcnvco  5996  f1eqcocnv  5997  acexmidlemcase  6080  nna0r  6751  nnawordex  6802  ectocld  6875  ecoptocl  6896  mapsnd  6970  mapsn  6972  eqeng  7052  fopwdom  7136  ordiso  7376  ltexnqq  7775  nsmallnqq  7779  nqprloc  7912  aptiprleml  8006  map2psrprg  8172  0re  8326  lttri3  8405  0cnALT  8516  reapti  8907  recnz  9739  zneo  9747  uzn0  9938  flqidz  10721  ceilqidz  10753  modqid2  10788  modqmuladdnn0  10805  frec2uzrand  10842  frecuzrdgtcl  10849  seq3id  10962  seq3z  10965  facdiv  11176  facwordi  11178  wrdnval  11335  wrdl1s1  11398  maxleb  11982  fsumf1o  12157  dvdsnegb  12575  odd2np1lem  12639  odd2np1  12640  ltoddhalfle  12660  halfleoddlt  12661  opoe  12662  omoe  12663  opeo  12664  omeo  12665  gcddiv  12796  gcdzeq  12799  dvdssqim  12801  lcmgcdeq  12861  coprmdvds2  12871  rpmul  12876  divgcdcoprmex  12880  cncongr2  12882  dvdsprm  12915  coprm  12922  prmdvdsexp  12926  prmdiv  13013  pythagtriplem19  13061  pc2dvds  13109  pcadd  13119  prmpwdvds  13134  exmidunben  13317  intopsn  13687  ismgmid  13697  imasmnd2  13759  isgrpid2  13845  isgrpinv  13859  dfgrp3mlem  13903  imasgrp2  13913  imasrng  14255  imasring  14369  dvdsrcl2  14406  dvdsrtr  14408  dvdsrmul1  14409  lspsneq0  14763  dvdsrzring  14938  znunit  14994  baspartn  15151  bastop  15176  isopn3  15226  pellexlem1  16091  lgsdir  16154  lgsne0  16157  lgsquadlem3  16198  uhgrm  16319  upgrfnen  16339  umgrfnen  16349  eupth2lem2dc  16700  eupth2lem3lem6fi  16712  bj-peano4  16981  sbthomlem  17070