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  1753  speimfwALT  1965  cbv1v  2340  cbv1  2406  hblem  2867  hblemg  2868  sbhypf  3502  axrep1  5225  axrep4v  5229  axrep4  5230  tfinds2  7806  smores  8284  idssen  8936  ssttrcl  9626  itunitc1  10332  dominf  10357  dominfac  10486  ssxr  11204  nnwos  12830  chnfibg  18561  pmatcollpw3lem  22729  ppttop  22953  ptclsg  23561  sincosq3sgn  26467  adjbdln  32160  fmptdF  32736  funcnv4mpt  32749  disjdsct  32784  esumpcvgval  34237  esumcvg  34245  measiuns  34376  ballotlemodife  34657  bnj605  35065  bnj594  35070  axreg  35285  axregs  35297  acycgr0v  35344  prclisacycgr  35347  imagesset  36149  meran1  36607  meran3  36609  mh-setind  36668  regsfromregtr  36670  regsfromunir1  36672  bj-modal4e  36918  f1omptsnlem  37543  mptsnunlem  37545  topdifinffinlem  37554  relowlpssretop  37571  poimirlem25  37848  eqbrb  38438  eqelb  38440  symrefref3  38843  dedths  39244  sn-axrep5v  42495  dffltz  42898  mzpincl  42997  lerabdioph  43068  ltrabdioph  43071  nerabdioph  43072  dvdsrabdioph  43073  finona1cl  43715  frege91  44216  frege97  44222  frege98  44223  frege109  44234  sumnnodd  45897  limsupvaluz2  46003  aiotaval  47362  rrx2linest  49009  fonex  49133