Theorem syl5ibcom 155

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

Hypotheses

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

Assertion

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

Proof of Theorem syl5ibcom

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

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  2987  rmob  3126  preqr1g  3854  issod  4422  sotritrieq  4428  nsuceq0g  4521  suctr  4524  nordeq  4648  suc11g  4661  iss  5065  poirr2  5136  xp11m  5182  tz6.12c  5678  fnbrfvb  5693  fvelimab  5711  foeqcnvco  5941  f1eqcocnv  5942  acexmidlemcase  6023  nna0r  6689  nnawordex  6740  ectocld  6813  ecoptocl  6834  mapsn  6902  eqeng  6982  fopwdom  7065  ordiso  7278  ltexnqq  7671  nsmallnqq  7675  nqprloc  7808  aptiprleml  7902  map2psrprg  8068  0re  8222  lttri3  8302  0cnALT  8412  reapti  8802  recnz  9616  zneo  9624  uzn0  9815  flqidz  10590  ceilqidz  10622  modqid2  10657  modqmuladdnn0  10674  frec2uzrand  10711  frecuzrdgtcl  10718  seq3id  10831  seq3z  10834  facdiv  11044  facwordi  11046  wrdnval  11191  wrdl1s1  11254  maxleb  11837  fsumf1o  12012  dvdsnegb  12430  odd2np1lem  12494  odd2np1  12495  ltoddhalfle  12515  halfleoddlt  12516  opoe  12517  omoe  12518  opeo  12519  omeo  12520  gcddiv  12651  gcdzeq  12654  dvdssqim  12656  lcmgcdeq  12716  coprmdvds2  12726  rpmul  12731  divgcdcoprmex  12735  cncongr2  12737  dvdsprm  12770  coprm  12777  prmdvdsexp  12781  prmdiv  12868  pythagtriplem19  12916  pc2dvds  12964  pcadd  12974  prmpwdvds  12989  exmidunben  13108  intopsn  13511  ismgmid  13521  imasmnd2  13596  isgrpid2  13684  isgrpinv  13698  dfgrp3mlem  13742  imasgrp2  13758  imasrng  14031  imasring  14139  dvdsrcl2  14175  dvdsrtr  14177  dvdsrmul1  14178  lspsneq0  14502  dvdsrzring  14679  znunit  14735  baspartn  14841  bastop  14866  isopn3  14916  pellexlem1  15771  lgsdir  15834  lgsne0  15837  lgsquadlem3  15878  uhgrm  15999  upgrfnen  16019  umgrfnen  16029  eupth2lem2dc  16380  eupth2lem3lem6fi  16392  bj-peano4  16651  sbthomlem  16733