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  2984  rmob  3123  preqr1g  3847  issod  4414  sotritrieq  4420  nsuceq0g  4513  suctr  4516  nordeq  4640  suc11g  4653  iss  5057  poirr2  5127  xp11m  5173  tz6.12c  5665  fnbrfvb  5680  fvelimab  5698  foeqcnvco  5926  f1eqcocnv  5927  acexmidlemcase  6008  nna0r  6641  nnawordex  6692  ectocld  6765  ecoptocl  6786  mapsn  6854  eqeng  6934  fopwdom  7017  ordiso  7229  ltexnqq  7621  nsmallnqq  7625  nqprloc  7758  aptiprleml  7852  map2psrprg  8018  0re  8172  lttri3  8252  0cnALT  8362  reapti  8752  recnz  9566  zneo  9574  uzn0  9765  flqidz  10539  ceilqidz  10571  modqid2  10606  modqmuladdnn0  10623  frec2uzrand  10660  frecuzrdgtcl  10667  seq3id  10780  seq3z  10783  facdiv  10993  facwordi  10995  wrdnval  11137  wrdl1s1  11200  maxleb  11770  fsumf1o  11944  dvdsnegb  12362  odd2np1lem  12426  odd2np1  12427  ltoddhalfle  12447  halfleoddlt  12448  opoe  12449  omoe  12450  opeo  12451  omeo  12452  gcddiv  12583  gcdzeq  12586  dvdssqim  12588  lcmgcdeq  12648  coprmdvds2  12658  rpmul  12663  divgcdcoprmex  12667  cncongr2  12669  dvdsprm  12702  coprm  12709  prmdvdsexp  12713  prmdiv  12800  pythagtriplem19  12848  pc2dvds  12896  pcadd  12906  prmpwdvds  12921  exmidunben  13040  intopsn  13443  ismgmid  13453  imasmnd2  13528  isgrpid2  13616  isgrpinv  13630  dfgrp3mlem  13674  imasgrp2  13690  imasrng  13962  imasring  14070  dvdsrcl2  14106  dvdsrtr  14108  dvdsrmul1  14109  lspsneq0  14433  dvdsrzring  14610  znunit  14666  baspartn  14767  bastop  14792  isopn3  14842  lgsdir  15757  lgsne0  15760  lgsquadlem3  15801  uhgrm  15922  upgrfnen  15942  umgrfnen  15952  bj-peano4  16500  sbthomlem  16579