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 ⊢ (𝜑 → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimpcd  159  mob2  3006  rmob  3145  preqr1g  3891  issod  4466  sotritrieq  4472  nsuceq0g  4565  suctr  4568  nordeq  4693  suc11g  4706  iss  5112  poirr2  5183  xp11m  5229  tz6.12c  5728  fnbrfvb  5744  fvelimab  5762  foeqcnvco  5999  f1eqcocnv  6000  acexmidlemcase  6083  nna0r  6756  nnawordex  6807  ectocld  6880  ecoptocl  6901  mapsnd  6976  mapsn  6978  eqeng  7058  fopwdom  7142  ordiso  7382  ltexnqq  7781  nsmallnqq  7785  nqprloc  7918  aptiprleml  8012  map2psrprg  8178  0re  8332  lttri3  8411  0cnALT  8523  reapti  8915  recnz  9749  zneo  9757  uzn0  9953  flqidz  10741  ceilqidz  10773  modqid2  10808  modqmuladdnn0  10825  frec2uzrand  10862  frecuzrdgtcl  10869  seq3id  10982  seq3z  10985  facdiv  11197  facwordi  11199  wrdnval  11356  wrdl1s1  11419  maxleb  12004  fsumf1o  12181  dvdsnegb  12599  odd2np1lem  12663  odd2np1  12664  ltoddhalfle  12684  halfleoddlt  12685  opoe  12686  omoe  12687  opeo  12688  omeo  12689  gcddiv  12820  gcdzeq  12823  dvdssqim  12825  lcmgcdeq  12885  coprmdvds2  12895  rpmul  12900  divgcdcoprmex  12904  cncongr2  12906  dvdsprm  12940  coprm  12947  prmdvdsexp  12951  prmdiv  13041  pythagtriplem19  13089  pc2dvds  13137  pcadd  13147  prmpwdvds  13162  exmidunben  13374  intopsn  13745  ismgmid  13755  imasmnd2  13817  isgrpid2  13903  isgrpinv  13917  dfgrp3mlem  13961  imasgrp2  13971  imasrng  14361  imasring  14477  dvdsrcl2  14514  dvdsrtr  14516  dvdsrmul1  14517  lspsneq0  14871  dvdsrzring  15046  znunit  15102  baspartn  15293  bastop  15318  isopn3  15368  pellexlem1  16246  ppiublem1  16308  lgsdir  16376  lgsne0  16379  lgsquadlem3  16420  uhgrm  16541  upgrfnen  16561  umgrfnen  16571  eupth2lem2dc  16922  eupth2lem3lem6fi  16934  bj-peano4  17203  sbthomlem  17293