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  2996  rmob  3135  preqr1g  3869  issod  4439  sotritrieq  4445  nsuceq0g  4538  suctr  4541  nordeq  4665  suc11g  4678  iss  5083  poirr2  5154  xp11m  5200  tz6.12c  5699  fnbrfvb  5714  fvelimab  5732  foeqcnvco  5962  f1eqcocnv  5963  acexmidlemcase  6044  nna0r  6710  nnawordex  6761  ectocld  6834  ecoptocl  6855  mapsnd  6922  mapsn  6924  eqeng  7004  fopwdom  7088  ordiso  7326  ltexnqq  7722  nsmallnqq  7726  nqprloc  7859  aptiprleml  7953  map2psrprg  8119  0re  8273  lttri3  8352  0cnALT  8462  reapti  8852  recnz  9670  zneo  9678  uzn0  9869  flqidz  10645  ceilqidz  10677  modqid2  10712  modqmuladdnn0  10729  frec2uzrand  10766  frecuzrdgtcl  10773  seq3id  10886  seq3z  10889  facdiv  11099  facwordi  11101  wrdnval  11251  wrdl1s1  11314  maxleb  11897  fsumf1o  12072  dvdsnegb  12490  odd2np1lem  12554  odd2np1  12555  ltoddhalfle  12575  halfleoddlt  12576  opoe  12577  omoe  12578  opeo  12579  omeo  12580  gcddiv  12711  gcdzeq  12714  dvdssqim  12716  lcmgcdeq  12776  coprmdvds2  12786  rpmul  12791  divgcdcoprmex  12795  cncongr2  12797  dvdsprm  12830  coprm  12837  prmdvdsexp  12841  prmdiv  12928  pythagtriplem19  12976  pc2dvds  13024  pcadd  13034  prmpwdvds  13049  exmidunben  13169  intopsn  13572  ismgmid  13582  imasmnd2  13657  isgrpid2  13745  isgrpinv  13759  dfgrp3mlem  13803  imasgrp2  13819  imasrng  14092  imasring  14200  dvdsrcl2  14236  dvdsrtr  14238  dvdsrmul1  14239  lspsneq0  14566  dvdsrzring  14743  znunit  14799  baspartn  14907  bastop  14932  isopn3  14982  pellexlem1  15837  lgsdir  15900  lgsne0  15903  lgsquadlem3  15944  uhgrm  16065  upgrfnen  16085  umgrfnen  16095  eupth2lem2dc  16446  eupth2lem3lem6fi  16458  bj-peano4  16717  sbthomlem  16797