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  8517  reapti  8909  recnz  9743  zneo  9751  uzn0  9947  flqidz  10734  ceilqidz  10766  modqid2  10801  modqmuladdnn0  10818  frec2uzrand  10855  frecuzrdgtcl  10862  seq3id  10975  seq3z  10978  facdiv  11190  facwordi  11192  wrdnval  11349  wrdl1s1  11412  maxleb  11997  fsumf1o  12173  dvdsnegb  12591  odd2np1lem  12655  odd2np1  12656  ltoddhalfle  12676  halfleoddlt  12677  opoe  12678  omoe  12679  opeo  12680  omeo  12681  gcddiv  12812  gcdzeq  12815  dvdssqim  12817  lcmgcdeq  12877  coprmdvds2  12887  rpmul  12892  divgcdcoprmex  12896  cncongr2  12898  dvdsprm  12932  coprm  12939  prmdvdsexp  12943  prmdiv  13033  pythagtriplem19  13081  pc2dvds  13129  pcadd  13139  prmpwdvds  13154  exmidunben  13366  intopsn  13736  ismgmid  13746  imasmnd2  13808  isgrpid2  13894  isgrpinv  13908  dfgrp3mlem  13952  imasgrp2  13962  imasrng  14304  imasring  14418  dvdsrcl2  14455  dvdsrtr  14457  dvdsrmul1  14458  lspsneq0  14812  dvdsrzring  14987  znunit  15043  baspartn  15200  bastop  15225  isopn3  15275  pellexlem1  16148  ppiublem1  16192  lgsdir  16252  lgsne0  16255  lgsquadlem3  16296  uhgrm  16417  upgrfnen  16437  umgrfnen  16447  eupth2lem2dc  16798  eupth2lem3lem6fi  16810  bj-peano4  17079  sbthomlem  17168