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  3843  issod  4407  sotritrieq  4413  nsuceq0g  4506  suctr  4509  nordeq  4633  suc11g  4646  iss  5047  poirr2  5117  xp11m  5163  tz6.12c  5653  fnbrfvb  5666  fvelimab  5683  foeqcnvco  5907  f1eqcocnv  5908  acexmidlemcase  5989  nna0r  6614  nnawordex  6665  ectocld  6738  ecoptocl  6759  mapsn  6827  eqeng  6907  fopwdom  6985  ordiso  7191  ltexnqq  7583  nsmallnqq  7587  nqprloc  7720  aptiprleml  7814  map2psrprg  7980  0re  8134  lttri3  8214  0cnALT  8324  reapti  8714  recnz  9528  zneo  9536  uzn0  9726  flqidz  10493  ceilqidz  10525  modqid2  10560  modqmuladdnn0  10577  frec2uzrand  10614  frecuzrdgtcl  10621  seq3id  10734  seq3z  10737  facdiv  10947  facwordi  10949  wrdnval  11088  wrdl1s1  11149  maxleb  11713  fsumf1o  11887  dvdsnegb  12305  odd2np1lem  12369  odd2np1  12370  ltoddhalfle  12390  halfleoddlt  12391  opoe  12392  omoe  12393  opeo  12394  omeo  12395  gcddiv  12526  gcdzeq  12529  dvdssqim  12531  lcmgcdeq  12591  coprmdvds2  12601  rpmul  12606  divgcdcoprmex  12610  cncongr2  12612  dvdsprm  12645  coprm  12652  prmdvdsexp  12656  prmdiv  12743  pythagtriplem19  12791  pc2dvds  12839  pcadd  12849  prmpwdvds  12864  exmidunben  12983  intopsn  13386  ismgmid  13396  imasmnd2  13471  isgrpid2  13559  isgrpinv  13573  dfgrp3mlem  13617  imasgrp2  13633  imasrng  13905  imasring  14013  dvdsrcl2  14048  dvdsrtr  14050  dvdsrmul1  14051  lspsneq0  14375  dvdsrzring  14552  znunit  14608  baspartn  14709  bastop  14734  isopn3  14784  lgsdir  15699  lgsne0  15702  lgsquadlem3  15743  uhgrm  15863  upgrfnen  15883  umgrfnen  15893  bj-peano4  16248  sbthomlem  16324