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  2983  rmob  3122  preqr1g  3844  issod  4410  sotritrieq  4416  nsuceq0g  4509  suctr  4512  nordeq  4636  suc11g  4649  iss  5051  poirr2  5121  xp11m  5167  tz6.12c  5659  fnbrfvb  5674  fvelimab  5692  foeqcnvco  5920  f1eqcocnv  5921  acexmidlemcase  6002  nna0r  6632  nnawordex  6683  ectocld  6756  ecoptocl  6777  mapsn  6845  eqeng  6925  fopwdom  7005  ordiso  7211  ltexnqq  7603  nsmallnqq  7607  nqprloc  7740  aptiprleml  7834  map2psrprg  8000  0re  8154  lttri3  8234  0cnALT  8344  reapti  8734  recnz  9548  zneo  9556  uzn0  9746  flqidz  10514  ceilqidz  10546  modqid2  10581  modqmuladdnn0  10598  frec2uzrand  10635  frecuzrdgtcl  10642  seq3id  10755  seq3z  10758  facdiv  10968  facwordi  10970  wrdnval  11110  wrdl1s1  11171  maxleb  11735  fsumf1o  11909  dvdsnegb  12327  odd2np1lem  12391  odd2np1  12392  ltoddhalfle  12412  halfleoddlt  12413  opoe  12414  omoe  12415  opeo  12416  omeo  12417  gcddiv  12548  gcdzeq  12551  dvdssqim  12553  lcmgcdeq  12613  coprmdvds2  12623  rpmul  12628  divgcdcoprmex  12632  cncongr2  12634  dvdsprm  12667  coprm  12674  prmdvdsexp  12678  prmdiv  12765  pythagtriplem19  12813  pc2dvds  12861  pcadd  12871  prmpwdvds  12886  exmidunben  13005  intopsn  13408  ismgmid  13418  imasmnd2  13493  isgrpid2  13581  isgrpinv  13595  dfgrp3mlem  13639  imasgrp2  13655  imasrng  13927  imasring  14035  dvdsrcl2  14071  dvdsrtr  14073  dvdsrmul1  14074  lspsneq0  14398  dvdsrzring  14575  znunit  14631  baspartn  14732  bastop  14757  isopn3  14807  lgsdir  15722  lgsne0  15725  lgsquadlem3  15766  uhgrm  15886  upgrfnen  15906  umgrfnen  15916  bj-peano4  16342  sbthomlem  16423