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  2940  rmob  3078  preqr1g  3792  issod  4350  sotritrieq  4356  nsuceq0g  4449  suctr  4452  nordeq  4576  suc11g  4589  iss  4988  poirr2  5058  xp11m  5104  tz6.12c  5584  fnbrfvb  5597  fvelimab  5613  foeqcnvco  5833  f1eqcocnv  5834  acexmidlemcase  5913  nna0r  6531  nnawordex  6582  ectocld  6655  ecoptocl  6676  mapsn  6744  eqeng  6820  fopwdom  6892  ordiso  7095  ltexnqq  7468  nsmallnqq  7472  nqprloc  7605  aptiprleml  7699  map2psrprg  7865  0re  8019  lttri3  8099  0cnALT  8209  reapti  8598  recnz  9410  zneo  9418  uzn0  9608  flqidz  10355  ceilqidz  10387  modqid2  10422  modqmuladdnn0  10439  frec2uzrand  10476  frecuzrdgtcl  10483  seq3id  10596  seq3z  10599  facdiv  10809  facwordi  10811  wrdnval  10944  maxleb  11360  fsumf1o  11533  dvdsnegb  11951  odd2np1lem  12013  odd2np1  12014  ltoddhalfle  12034  halfleoddlt  12035  opoe  12036  omoe  12037  opeo  12038  omeo  12039  gcddiv  12156  gcdzeq  12159  dvdssqim  12161  lcmgcdeq  12221  coprmdvds2  12231  rpmul  12236  divgcdcoprmex  12240  cncongr2  12242  dvdsprm  12275  coprm  12282  prmdvdsexp  12286  prmdiv  12373  pythagtriplem19  12420  pc2dvds  12468  pcadd  12478  prmpwdvds  12493  exmidunben  12583  intopsn  12950  ismgmid  12960  isgrpid2  13112  isgrpinv  13126  dfgrp3mlem  13170  imasgrp2  13180  imasrng  13452  imasring  13560  dvdsrcl2  13595  dvdsrtr  13597  dvdsrmul1  13598  lspsneq0  13922  dvdsrzring  14091  znunit  14147  baspartn  14218  bastop  14243  isopn3  14293  lgsdir  15151  lgsne0  15154  bj-peano4  15447  sbthomlem  15515