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  3000  rmob  3139  preqr1g  3875  issod  4445  sotritrieq  4451  nsuceq0g  4544  suctr  4547  nordeq  4671  suc11g  4684  iss  5089  poirr2  5160  xp11m  5206  tz6.12c  5705  fnbrfvb  5720  fvelimab  5738  foeqcnvco  5969  f1eqcocnv  5970  acexmidlemcase  6053  nna0r  6724  nnawordex  6775  ectocld  6848  ecoptocl  6869  mapsnd  6936  mapsn  6938  eqeng  7018  fopwdom  7102  ordiso  7340  ltexnqq  7739  nsmallnqq  7743  nqprloc  7876  aptiprleml  7970  map2psrprg  8136  0re  8290  lttri3  8369  0cnALT  8479  reapti  8870  recnz  9689  zneo  9697  uzn0  9888  flqidz  10670  ceilqidz  10702  modqid2  10737  modqmuladdnn0  10754  frec2uzrand  10791  frecuzrdgtcl  10798  seq3id  10911  seq3z  10914  facdiv  11125  facwordi  11127  wrdnval  11280  wrdl1s1  11343  maxleb  11926  fsumf1o  12101  dvdsnegb  12519  odd2np1lem  12583  odd2np1  12584  ltoddhalfle  12604  halfleoddlt  12605  opoe  12606  omoe  12607  opeo  12608  omeo  12609  gcddiv  12740  gcdzeq  12743  dvdssqim  12745  lcmgcdeq  12805  coprmdvds2  12815  rpmul  12820  divgcdcoprmex  12824  cncongr2  12826  dvdsprm  12859  coprm  12866  prmdvdsexp  12870  prmdiv  12957  pythagtriplem19  13005  pc2dvds  13053  pcadd  13063  prmpwdvds  13078  exmidunben  13261  intopsn  13664  ismgmid  13674  imasmnd2  13749  isgrpid2  13837  isgrpinv  13851  dfgrp3mlem  13895  imasgrp2  13911  imasrng  14184  imasring  14292  dvdsrcl2  14329  dvdsrtr  14331  dvdsrmul1  14332  lspsneq0  14686  dvdsrzring  14863  znunit  14919  baspartn  15027  bastop  15052  isopn3  15102  pellexlem1  15957  lgsdir  16020  lgsne0  16023  lgsquadlem3  16064  uhgrm  16185  upgrfnen  16205  umgrfnen  16215  eupth2lem2dc  16566  eupth2lem3lem6fi  16578  bj-peano4  16837  sbthomlem  16917