Theorem 3imtr3i 291

Description: A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.)

Hypotheses

Ref	Expression
3imtr3.1	⊢ (𝜑 → 𝜓)
3imtr3.2	⊢ (𝜑 ↔ 𝜒)
3imtr3.3	⊢ (𝜓 ↔ 𝜃)

Assertion

Ref	Expression
3imtr3i	⊢ (𝜒 → 𝜃)

Proof of Theorem 3imtr3i

Step	Hyp	Ref	Expression
1		3imtr3.2	. . 3 ⊢ (𝜑 ↔ 𝜒)
2		3imtr3.1	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	sylbir 235	. 2 ⊢ (𝜒 → 𝜓)
4		3imtr3.3	. 2 ⊢ (𝜓 ↔ 𝜃)
5	3, 4	sylib 218	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  rb-ax1  1752  speimfwALT  1964  cbv1v  2334  cbv1  2400  hblem  2859  hblemg  2860  sbhypf  3499  axrep1  5219  axrep4v  5223  axrep4  5224  tfinds2  7797  smores  8275  idssen  8922  ssttrcl  9611  itunitc1  10314  dominf  10339  dominfac  10467  ssxr  11185  nnwos  12816  pmatcollpw3lem  22668  ppttop  22892  ptclsg  23500  sincosq3sgn  26407  adjbdln  32027  fmptdF  32600  funcnv4mpt  32613  disjdsct  32646  esumpcvgval  34051  esumcvg  34059  measiuns  34190  ballotlemodife  34472  bnj605  34880  bnj594  34885  axreg  35068  axregs  35084  acycgr0v  35131  prclisacycgr  35134  imagesset  35937  meran1  36395  meran3  36397  bj-modal4e  36699  f1omptsnlem  37320  mptsnunlem  37322  topdifinffinlem  37331  relowlpssretop  37348  poimirlem25  37635  eqbrb  38217  eqelb  38219  symrefref3  38551  dedths  38951  sn-axrep5v  42199  dffltz  42617  mzpincl  42717  lerabdioph  42788  ltrabdioph  42791  nerabdioph  42792  dvdsrabdioph  42793  finona1cl  43436  frege91  43937  frege97  43943  frege98  43944  frege109  43955  sumnnodd  45621  limsupvaluz2  45729  aiotaval  47089  rrx2linest  48737  fonex  48861