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  1754  speimfwALT  1966  cbv1v  2341  cbv1  2407  hblem  2868  hblemg  2869  sbhypf  3504  axrep1  5227  axrep4v  5231  axrep4  5232  tfinds2  7816  smores  8294  idssen  8946  ssttrcl  9636  itunitc1  10342  dominf  10367  dominfac  10496  ssxr  11214  nnwos  12840  chnfibg  18571  pmatcollpw3lem  22742  ppttop  22966  ptclsg  23574  sincosq3sgn  26480  adjbdln  32175  fmptdF  32750  funcnv4mpt  32762  disjdsct  32797  esumpcvgval  34260  esumcvg  34268  measiuns  34399  ballotlemodife  34680  bnj605  35087  bnj594  35092  axreg  35309  axregs  35321  acycgr0v  35368  prclisacycgr  35371  imagesset  36173  meran1  36631  meran3  36633  mh-setind  36692  regsfromregtr  36694  regsfromunir1  36696  bj-modal4e  36964  f1omptsnlem  37595  mptsnunlem  37597  topdifinffinlem  37606  relowlpssretop  37623  poimirlem25  37900  eqbrb  38494  eqelb  38496  symrefref3  38903  dedths  39342  sn-axrep5v  42593  dffltz  42996  mzpincl  43095  lerabdioph  43166  ltrabdioph  43169  nerabdioph  43170  dvdsrabdioph  43171  finona1cl  43813  frege91  44314  frege97  44320  frege98  44321  frege109  44332  sumnnodd  45994  limsupvaluz2  46100  aiotaval  47459  rrx2linest  49106  fonex  49230