Theorem syl5ibcom 154

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

Hypotheses

Ref	Expression
syl5ib.1	⊢ (𝜑 → 𝜓)
syl5ib.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ibcom	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem syl5ibcom

Step	Hyp	Ref	Expression
1		syl5ib.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl5ib.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	syl5ib 153	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	com12 30	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpcd  158  mob2  2796  rmob  2932  preqr1g  3616  issod  4155  sotritrieq  4161  nsuceq0g  4254  suctr  4257  nordeq  4373  suc11g  4386  iss  4771  poirr2  4837  xp11m  4882  tz6.12c  5347  fnbrfvb  5358  fvelimab  5373  foeqcnvco  5583  f1eqcocnv  5584  acexmidlemcase  5661  nna0r  6253  nnawordex  6301  ectocld  6372  ecoptocl  6393  mapsn  6461  eqeng  6537  fopwdom  6606  ordiso  6783  ltexnqq  7021  nsmallnqq  7025  nqprloc  7158  aptiprleml  7252  0re  7542  lttri3  7619  0cnALT  7726  reapti  8110  recnz  8893  zneo  8901  uzn0  9088  flqidz  9747  ceilqidz  9777  modqid2  9812  modqmuladdnn0  9829  frec2uzrand  9866  frecuzrdgtcl  9873  iseqid  9993  iseqz  9997  facdiv  10200  facwordi  10202  maxleb  10703  fsumf1o  10836  dvdsnegb  11145  odd2np1lem  11204  odd2np1  11205  ltoddhalfle  11225  halfleoddlt  11226  opoe  11227  omoe  11228  opeo  11229  omeo  11230  gcddiv  11340  gcdzeq  11343  dvdssqim  11345  lcmgcdeq  11397  coprmdvds2  11407  rpmul  11412  divgcdcoprmex  11416  cncongr2  11418  dvdsprm  11450  coprm  11455  prmdvdsexp  11459  baspartn  11802  bastop  11829  isopn3  11879  bj-peano4  12116