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  2919  rmob  3057  preqr1g  3768  issod  4321  sotritrieq  4327  nsuceq0g  4420  suctr  4423  nordeq  4545  suc11g  4558  iss  4955  poirr2  5023  xp11m  5069  tz6.12c  5547  fnbrfvb  5559  fvelimab  5575  foeqcnvco  5794  f1eqcocnv  5795  acexmidlemcase  5873  nna0r  6482  nnawordex  6533  ectocld  6604  ecoptocl  6625  mapsn  6693  eqeng  6769  fopwdom  6839  ordiso  7038  ltexnqq  7410  nsmallnqq  7414  nqprloc  7547  aptiprleml  7641  map2psrprg  7807  0re  7960  lttri3  8040  0cnALT  8150  reapti  8539  recnz  9349  zneo  9357  uzn0  9546  flqidz  10289  ceilqidz  10319  modqid2  10354  modqmuladdnn0  10371  frec2uzrand  10408  frecuzrdgtcl  10415  seq3id  10511  seq3z  10514  facdiv  10721  facwordi  10723  maxleb  11228  fsumf1o  11401  dvdsnegb  11818  odd2np1lem  11880  odd2np1  11881  ltoddhalfle  11901  halfleoddlt  11902  opoe  11903  omoe  11904  opeo  11905  omeo  11906  gcddiv  12023  gcdzeq  12026  dvdssqim  12028  lcmgcdeq  12086  coprmdvds2  12096  rpmul  12101  divgcdcoprmex  12105  cncongr2  12107  dvdsprm  12140  coprm  12147  prmdvdsexp  12151  prmdiv  12238  pythagtriplem19  12285  pc2dvds  12332  pcadd  12342  prmpwdvds  12356  exmidunben  12430  intopsn  12792  ismgmid  12802  isgrpid2  12919  isgrpinv  12932  dfgrp3mlem  12974  dvdsrcl2  13274  dvdsrtr  13276  dvdsrmul1  13277  lspsneq0  13518  dvdsrzring  13633  baspartn  13690  bastop  13715  isopn3  13765  lgsdir  14576  lgsne0  14579  bj-peano4  14847  sbthomlem  14914