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 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimpcd  159  mob2  3006  rmob  3145  preqr1g  3891  issod  4464  sotritrieq  4470  nsuceq0g  4563  suctr  4566  nordeq  4691  suc11g  4704  iss  5109  poirr2  5180  xp11m  5226  tz6.12c  5725  fnbrfvb  5741  fvelimab  5759  foeqcnvco  5996  f1eqcocnv  5997  acexmidlemcase  6080  nna0r  6751  nnawordex  6802  ectocld  6875  ecoptocl  6896  mapsnd  6970  mapsn  6972  eqeng  7052  fopwdom  7136  ordiso  7376  ltexnqq  7775  nsmallnqq  7779  nqprloc  7912  aptiprleml  8006  map2psrprg  8172  0re  8326  lttri3  8405  0cnALT  8516  reapti  8908  recnz  9741  zneo  9749  uzn0  9940  flqidz  10723  ceilqidz  10755  modqid2  10790  modqmuladdnn0  10807  frec2uzrand  10844  frecuzrdgtcl  10851  seq3id  10964  seq3z  10967  facdiv  11178  facwordi  11180  wrdnval  11337  wrdl1s1  11400  maxleb  11984  fsumf1o  12159  dvdsnegb  12577  odd2np1lem  12641  odd2np1  12642  ltoddhalfle  12662  halfleoddlt  12663  opoe  12664  omoe  12665  opeo  12666  omeo  12667  gcddiv  12798  gcdzeq  12801  dvdssqim  12803  lcmgcdeq  12863  coprmdvds2  12873  rpmul  12878  divgcdcoprmex  12882  cncongr2  12884  dvdsprm  12917  coprm  12924  prmdvdsexp  12928  prmdiv  13015  pythagtriplem19  13063  pc2dvds  13111  pcadd  13121  prmpwdvds  13136  exmidunben  13319  intopsn  13689  ismgmid  13699  imasmnd2  13761  isgrpid2  13847  isgrpinv  13861  dfgrp3mlem  13905  imasgrp2  13915  imasrng  14257  imasring  14371  dvdsrcl2  14408  dvdsrtr  14410  dvdsrmul1  14411  lspsneq0  14765  dvdsrzring  14940  znunit  14996  baspartn  15153  bastop  15178  isopn3  15228  pellexlem1  16097  lgsdir  16166  lgsne0  16169  lgsquadlem3  16210  uhgrm  16331  upgrfnen  16351  umgrfnen  16361  eupth2lem2dc  16712  eupth2lem3lem6fi  16724  bj-peano4  16993  sbthomlem  17082