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  5558  fvelimab  5574  foeqcnvco  5793  f1eqcocnv  5794  acexmidlemcase  5872  nna0r  6481  nnawordex  6532  ectocld  6603  ecoptocl  6624  mapsn  6692  eqeng  6768  fopwdom  6838  ordiso  7037  ltexnqq  7409  nsmallnqq  7413  nqprloc  7546  aptiprleml  7640  map2psrprg  7806  0re  7959  lttri3  8039  0cnALT  8149  reapti  8538  recnz  9348  zneo  9356  uzn0  9545  flqidz  10288  ceilqidz  10318  modqid2  10353  modqmuladdnn0  10370  frec2uzrand  10407  frecuzrdgtcl  10414  seq3id  10510  seq3z  10513  facdiv  10720  facwordi  10722  maxleb  11227  fsumf1o  11400  dvdsnegb  11817  odd2np1lem  11879  odd2np1  11880  ltoddhalfle  11900  halfleoddlt  11901  opoe  11902  omoe  11903  opeo  11904  omeo  11905  gcddiv  12022  gcdzeq  12025  dvdssqim  12027  lcmgcdeq  12085  coprmdvds2  12095  rpmul  12100  divgcdcoprmex  12104  cncongr2  12106  dvdsprm  12139  coprm  12146  prmdvdsexp  12150  prmdiv  12237  pythagtriplem19  12284  pc2dvds  12331  pcadd  12341  prmpwdvds  12355  exmidunben  12429  intopsn  12791  ismgmid  12801  isgrpid2  12918  isgrpinv  12931  dfgrp3mlem  12973  dvdsrcl2  13273  dvdsrtr  13275  dvdsrmul1  13276  dvdsrzring  13532  baspartn  13589  bastop  13614  isopn3  13664  lgsdir  14475  lgsne0  14478  bj-peano4  14746  sbthomlem  14812