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  2955  rmob  3093  preqr1g  3810  issod  4371  sotritrieq  4377  nsuceq0g  4470  suctr  4473  nordeq  4597  suc11g  4610  iss  5011  poirr2  5081  xp11m  5127  tz6.12c  5616  fnbrfvb  5629  fvelimab  5645  foeqcnvco  5869  f1eqcocnv  5870  acexmidlemcase  5949  nna0r  6574  nnawordex  6625  ectocld  6698  ecoptocl  6719  mapsn  6787  eqeng  6867  fopwdom  6945  ordiso  7150  ltexnqq  7534  nsmallnqq  7538  nqprloc  7671  aptiprleml  7765  map2psrprg  7931  0re  8085  lttri3  8165  0cnALT  8275  reapti  8665  recnz  9479  zneo  9487  uzn0  9677  flqidz  10442  ceilqidz  10474  modqid2  10509  modqmuladdnn0  10526  frec2uzrand  10563  frecuzrdgtcl  10570  seq3id  10683  seq3z  10686  facdiv  10896  facwordi  10898  wrdnval  11037  wrdl1s1  11098  maxleb  11577  fsumf1o  11751  dvdsnegb  12169  odd2np1lem  12233  odd2np1  12234  ltoddhalfle  12254  halfleoddlt  12255  opoe  12256  omoe  12257  opeo  12258  omeo  12259  gcddiv  12390  gcdzeq  12393  dvdssqim  12395  lcmgcdeq  12455  coprmdvds2  12465  rpmul  12470  divgcdcoprmex  12474  cncongr2  12476  dvdsprm  12509  coprm  12516  prmdvdsexp  12520  prmdiv  12607  pythagtriplem19  12655  pc2dvds  12703  pcadd  12713  prmpwdvds  12728  exmidunben  12847  intopsn  13249  ismgmid  13259  imasmnd2  13334  isgrpid2  13422  isgrpinv  13436  dfgrp3mlem  13480  imasgrp2  13496  imasrng  13768  imasring  13876  dvdsrcl2  13911  dvdsrtr  13913  dvdsrmul1  13914  lspsneq0  14238  dvdsrzring  14415  znunit  14471  baspartn  14572  bastop  14597  isopn3  14647  lgsdir  15562  lgsne0  15565  lgsquadlem3  15606  uhgrm  15724  upgrfnen  15744  umgrfnen  15754  bj-peano4  16005  sbthomlem  16079