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  2944  rmob  3082  preqr1g  3797  issod  4355  sotritrieq  4361  nsuceq0g  4454  suctr  4457  nordeq  4581  suc11g  4594  iss  4993  poirr2  5063  xp11m  5109  tz6.12c  5591  fnbrfvb  5604  fvelimab  5620  foeqcnvco  5840  f1eqcocnv  5841  acexmidlemcase  5920  nna0r  6545  nnawordex  6596  ectocld  6669  ecoptocl  6690  mapsn  6758  eqeng  6834  fopwdom  6906  ordiso  7111  ltexnqq  7492  nsmallnqq  7496  nqprloc  7629  aptiprleml  7723  map2psrprg  7889  0re  8043  lttri3  8123  0cnALT  8233  reapti  8623  recnz  9436  zneo  9444  uzn0  9634  flqidz  10393  ceilqidz  10425  modqid2  10460  modqmuladdnn0  10477  frec2uzrand  10514  frecuzrdgtcl  10521  seq3id  10634  seq3z  10637  facdiv  10847  facwordi  10849  wrdnval  10982  maxleb  11398  fsumf1o  11572  dvdsnegb  11990  odd2np1lem  12054  odd2np1  12055  ltoddhalfle  12075  halfleoddlt  12076  opoe  12077  omoe  12078  opeo  12079  omeo  12080  gcddiv  12211  gcdzeq  12214  dvdssqim  12216  lcmgcdeq  12276  coprmdvds2  12286  rpmul  12291  divgcdcoprmex  12295  cncongr2  12297  dvdsprm  12330  coprm  12337  prmdvdsexp  12341  prmdiv  12428  pythagtriplem19  12476  pc2dvds  12524  pcadd  12534  prmpwdvds  12549  exmidunben  12668  intopsn  13069  ismgmid  13079  imasmnd2  13154  isgrpid2  13242  isgrpinv  13256  dfgrp3mlem  13300  imasgrp2  13316  imasrng  13588  imasring  13696  dvdsrcl2  13731  dvdsrtr  13733  dvdsrmul1  13734  lspsneq0  14058  dvdsrzring  14235  znunit  14291  baspartn  14370  bastop  14395  isopn3  14445  lgsdir  15360  lgsne0  15363  lgsquadlem3  15404  bj-peano4  15685  sbthomlem  15756