Theorem syl5ibcom 154

Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)

Hypotheses

Ref	Expression
syl5ib.1	|- ( ph -> ps )
syl5ib.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
syl5ibcom	|- ( ph -> ( ch -> th ) )

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		syl5ib.1	. . 3 |- ( ph -> ps )
2		syl5ib.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	1, 2	syl5ib 153	. 2 |- ( ch -> ( ph -> th ) )
4	3	com12 30	1 |- ( ph -> ( ch -> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpcd  158  mob2  2868  rmob  3005  preqr1g  3701  issod  4249  sotritrieq  4255  nsuceq0g  4348  suctr  4351  nordeq  4467  suc11g  4480  iss  4873  poirr2  4939  xp11m  4985  tz6.12c  5459  fnbrfvb  5470  fvelimab  5485  foeqcnvco  5699  f1eqcocnv  5700  acexmidlemcase  5777  nna0r  6382  nnawordex  6432  ectocld  6503  ecoptocl  6524  mapsn  6592  eqeng  6668  fopwdom  6738  ordiso  6929  ltexnqq  7240  nsmallnqq  7244  nqprloc  7377  aptiprleml  7471  map2psrprg  7637  0re  7790  lttri3  7868  0cnALT  7976  reapti  8365  recnz  9168  zneo  9176  uzn0  9365  flqidz  10090  ceilqidz  10120  modqid2  10155  modqmuladdnn0  10172  frec2uzrand  10209  frecuzrdgtcl  10216  seq3id  10312  seq3z  10315  facdiv  10516  facwordi  10518  maxleb  11020  fsumf1o  11191  dvdsnegb  11546  odd2np1lem  11605  odd2np1  11606  ltoddhalfle  11626  halfleoddlt  11627  opoe  11628  omoe  11629  opeo  11630  omeo  11631  gcddiv  11743  gcdzeq  11746  dvdssqim  11748  lcmgcdeq  11800  coprmdvds2  11810  rpmul  11815  divgcdcoprmex  11819  cncongr2  11821  dvdsprm  11853  coprm  11858  prmdvdsexp  11862  exmidunben  11975  baspartn  12256  bastop  12283  isopn3  12333  bj-peano4  13324  sbthomlem  13395