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  3876  issod  4446  sotritrieq  4452  nsuceq0g  4545  suctr  4548  nordeq  4673  suc11g  4686  iss  5091  poirr2  5162  xp11m  5208  tz6.12c  5707  fnbrfvb  5722  fvelimab  5740  foeqcnvco  5971  f1eqcocnv  5972  acexmidlemcase  6055  nna0r  6726  nnawordex  6777  ectocld  6850  ecoptocl  6871  mapsnd  6938  mapsn  6940  eqeng  7020  fopwdom  7104  ordiso  7342  ltexnqq  7741  nsmallnqq  7745  nqprloc  7878  aptiprleml  7972  map2psrprg  8138  0re  8292  lttri3  8371  0cnALT  8482  reapti  8873  recnz  9694  zneo  9702  uzn0  9893  flqidz  10675  ceilqidz  10707  modqid2  10742  modqmuladdnn0  10759  frec2uzrand  10796  frecuzrdgtcl  10803  seq3id  10916  seq3z  10919  facdiv  11130  facwordi  11132  wrdnval  11285  wrdl1s1  11348  maxleb  11932  fsumf1o  12107  dvdsnegb  12525  odd2np1lem  12589  odd2np1  12590  ltoddhalfle  12610  halfleoddlt  12611  opoe  12612  omoe  12613  opeo  12614  omeo  12615  gcddiv  12746  gcdzeq  12749  dvdssqim  12751  lcmgcdeq  12811  coprmdvds2  12821  rpmul  12826  divgcdcoprmex  12830  cncongr2  12832  dvdsprm  12865  coprm  12872  prmdvdsexp  12876  prmdiv  12963  pythagtriplem19  13011  pc2dvds  13059  pcadd  13069  prmpwdvds  13084  exmidunben  13267  intopsn  13636  ismgmid  13646  imasmnd2  13708  isgrpid2  13794  isgrpinv  13808  dfgrp3mlem  13852  imasgrp2  13862  imasrng  14202  imasring  14314  dvdsrcl2  14351  dvdsrtr  14353  dvdsrmul1  14354  lspsneq0  14707  dvdsrzring  14882  znunit  14938  baspartn  15046  bastop  15071  isopn3  15121  pellexlem1  15976  lgsdir  16039  lgsne0  16042  lgsquadlem3  16083  uhgrm  16204  upgrfnen  16224  umgrfnen  16234  eupth2lem2dc  16585  eupth2lem3lem6fi  16597  bj-peano4  16866  sbthomlem  16946