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  7377  ltexnqq  7776  nsmallnqq  7780  nqprloc  7913  aptiprleml  8007  map2psrprg  8173  0re  8327  lttri3  8406  0cnALT  8518  reapti  8910  recnz  9744  zneo  9752  uzn0  9948  flqidz  10736  ceilqidz  10768  modqid2  10803  modqmuladdnn0  10820  frec2uzrand  10857  frecuzrdgtcl  10864  seq3id  10977  seq3z  10980  facdiv  11192  facwordi  11194  wrdnval  11351  wrdl1s1  11414  maxleb  11999  fsumf1o  12176  dvdsnegb  12594  odd2np1lem  12658  odd2np1  12659  ltoddhalfle  12679  halfleoddlt  12680  opoe  12681  omoe  12682  opeo  12683  omeo  12684  gcddiv  12815  gcdzeq  12818  dvdssqim  12820  lcmgcdeq  12880  coprmdvds2  12890  rpmul  12895  divgcdcoprmex  12899  cncongr2  12901  dvdsprm  12935  coprm  12942  prmdvdsexp  12946  prmdiv  13036  pythagtriplem19  13084  pc2dvds  13132  pcadd  13142  prmpwdvds  13157  exmidunben  13369  intopsn  13739  ismgmid  13749  imasmnd2  13811  isgrpid2  13897  isgrpinv  13911  dfgrp3mlem  13955  imasgrp2  13965  imasrng  14307  imasring  14421  dvdsrcl2  14458  dvdsrtr  14460  dvdsrmul1  14461  lspsneq0  14815  dvdsrzring  14990  znunit  15046  baspartn  15210  bastop  15235  isopn3  15285  pellexlem1  16158  ppiublem1  16220  lgsdir  16288  lgsne0  16291  lgsquadlem3  16332  uhgrm  16453  upgrfnen  16473  umgrfnen  16483  eupth2lem2dc  16834  eupth2lem3lem6fi  16846  bj-peano4  17115  sbthomlem  17204