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  2986  rmob  3125  preqr1g  3849  issod  4416  sotritrieq  4422  nsuceq0g  4515  suctr  4518  nordeq  4642  suc11g  4655  iss  5059  poirr2  5129  xp11m  5175  tz6.12c  5669  fnbrfvb  5684  fvelimab  5702  foeqcnvco  5931  f1eqcocnv  5932  acexmidlemcase  6013  nna0r  6646  nnawordex  6697  ectocld  6770  ecoptocl  6791  mapsn  6859  eqeng  6939  fopwdom  7022  ordiso  7235  ltexnqq  7628  nsmallnqq  7632  nqprloc  7765  aptiprleml  7859  map2psrprg  8025  0re  8179  lttri3  8259  0cnALT  8369  reapti  8759  recnz  9573  zneo  9581  uzn0  9772  flqidz  10547  ceilqidz  10579  modqid2  10614  modqmuladdnn0  10631  frec2uzrand  10668  frecuzrdgtcl  10675  seq3id  10788  seq3z  10791  facdiv  11001  facwordi  11003  wrdnval  11148  wrdl1s1  11211  maxleb  11781  fsumf1o  11956  dvdsnegb  12374  odd2np1lem  12438  odd2np1  12439  ltoddhalfle  12459  halfleoddlt  12460  opoe  12461  omoe  12462  opeo  12463  omeo  12464  gcddiv  12595  gcdzeq  12598  dvdssqim  12600  lcmgcdeq  12660  coprmdvds2  12670  rpmul  12675  divgcdcoprmex  12679  cncongr2  12681  dvdsprm  12714  coprm  12721  prmdvdsexp  12725  prmdiv  12812  pythagtriplem19  12860  pc2dvds  12908  pcadd  12918  prmpwdvds  12933  exmidunben  13052  intopsn  13455  ismgmid  13465  imasmnd2  13540  isgrpid2  13628  isgrpinv  13642  dfgrp3mlem  13686  imasgrp2  13702  imasrng  13975  imasring  14083  dvdsrcl2  14119  dvdsrtr  14121  dvdsrmul1  14122  lspsneq0  14446  dvdsrzring  14623  znunit  14679  baspartn  14780  bastop  14805  isopn3  14855  lgsdir  15770  lgsne0  15773  lgsquadlem3  15814  uhgrm  15935  upgrfnen  15955  umgrfnen  15965  eupth2lem2dc  16316  eupth2lem3lem6fi  16328  bj-peano4  16576  sbthomlem  16655