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  3006  rmob  3145  preqr1g  3889  issod  4462  sotritrieq  4468  nsuceq0g  4561  suctr  4564  nordeq  4689  suc11g  4702  iss  5107  poirr2  5178  xp11m  5224  tz6.12c  5723  fnbrfvb  5738  fvelimab  5756  foeqcnvco  5990  f1eqcocnv  5991  acexmidlemcase  6074  nna0r  6745  nnawordex  6796  ectocld  6869  ecoptocl  6890  mapsnd  6964  mapsn  6966  eqeng  7046  fopwdom  7130  ordiso  7370  ltexnqq  7769  nsmallnqq  7773  nqprloc  7906  aptiprleml  8000  map2psrprg  8166  0re  8320  lttri3  8399  0cnALT  8510  reapti  8901  recnz  9722  zneo  9730  uzn0  9921  flqidz  10704  ceilqidz  10736  modqid2  10771  modqmuladdnn0  10788  frec2uzrand  10825  frecuzrdgtcl  10832  seq3id  10945  seq3z  10948  facdiv  11159  facwordi  11161  wrdnval  11318  wrdl1s1  11381  maxleb  11965  fsumf1o  12140  dvdsnegb  12558  odd2np1lem  12622  odd2np1  12623  ltoddhalfle  12643  halfleoddlt  12644  opoe  12645  omoe  12646  opeo  12647  omeo  12648  gcddiv  12779  gcdzeq  12782  dvdssqim  12784  lcmgcdeq  12844  coprmdvds2  12854  rpmul  12859  divgcdcoprmex  12863  cncongr2  12865  dvdsprm  12898  coprm  12905  prmdvdsexp  12909  prmdiv  12996  pythagtriplem19  13044  pc2dvds  13092  pcadd  13102  prmpwdvds  13117  exmidunben  13300  intopsn  13670  ismgmid  13680  imasmnd2  13742  isgrpid2  13828  isgrpinv  13842  dfgrp3mlem  13886  imasgrp2  13896  imasrng  14238  imasring  14352  dvdsrcl2  14389  dvdsrtr  14391  dvdsrmul1  14392  lspsneq0  14746  dvdsrzring  14921  znunit  14977  baspartn  15134  bastop  15159  isopn3  15209  pellexlem1  16074  lgsdir  16137  lgsne0  16140  lgsquadlem3  16181  uhgrm  16302  upgrfnen  16322  umgrfnen  16332  eupth2lem2dc  16683  eupth2lem3lem6fi  16695  bj-peano4  16964  sbthomlem  17044