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  2944  rmob  3082  preqr1g  3796  issod  4354  sotritrieq  4360  nsuceq0g  4453  suctr  4456  nordeq  4580  suc11g  4593  iss  4992  poirr2  5062  xp11m  5108  tz6.12c  5588  fnbrfvb  5601  fvelimab  5617  foeqcnvco  5837  f1eqcocnv  5838  acexmidlemcase  5917  nna0r  6536  nnawordex  6587  ectocld  6660  ecoptocl  6681  mapsn  6749  eqeng  6825  fopwdom  6897  ordiso  7102  ltexnqq  7475  nsmallnqq  7479  nqprloc  7612  aptiprleml  7706  map2psrprg  7872  0re  8026  lttri3  8106  0cnALT  8216  reapti  8606  recnz  9419  zneo  9427  uzn0  9617  flqidz  10376  ceilqidz  10408  modqid2  10443  modqmuladdnn0  10460  frec2uzrand  10497  frecuzrdgtcl  10504  seq3id  10617  seq3z  10620  facdiv  10830  facwordi  10832  wrdnval  10965  maxleb  11381  fsumf1o  11555  dvdsnegb  11973  odd2np1lem  12037  odd2np1  12038  ltoddhalfle  12058  halfleoddlt  12059  opoe  12060  omoe  12061  opeo  12062  omeo  12063  gcddiv  12186  gcdzeq  12189  dvdssqim  12191  lcmgcdeq  12251  coprmdvds2  12261  rpmul  12266  divgcdcoprmex  12270  cncongr2  12272  dvdsprm  12305  coprm  12312  prmdvdsexp  12316  prmdiv  12403  pythagtriplem19  12451  pc2dvds  12499  pcadd  12509  prmpwdvds  12524  exmidunben  12643  intopsn  13010  ismgmid  13020  isgrpid2  13172  isgrpinv  13186  dfgrp3mlem  13230  imasgrp2  13240  imasrng  13512  imasring  13620  dvdsrcl2  13655  dvdsrtr  13657  dvdsrmul1  13658  lspsneq0  13982  dvdsrzring  14159  znunit  14215  baspartn  14286  bastop  14311  isopn3  14361  lgsdir  15276  lgsne0  15279  lgsquadlem3  15320  bj-peano4  15601  sbthomlem  15669