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  2340  cbv1  2406  hblem  2867  hblemg  2868  sbhypf  3490  axrep1  5213  axrep4v  5217  axrep4  5218  tfinds2  7815  smores  8292  idssen  8944  ssttrcl  9636  itunitc1  10342  dominf  10367  dominfac  10496  ssxr  11215  nnwos  12865  chnfibg  18602  pmatcollpw3lem  22748  ppttop  22972  ptclsg  23580  sincosq3sgn  26464  adjbdln  32154  fmptdF  32729  funcnv4mpt  32741  disjdsct  32776  esumpcvgval  34222  esumcvg  34230  measiuns  34361  ballotlemodife  34642  bnj605  35049  bnj594  35054  axreg  35271  axregs  35283  acycgr0v  35330  prclisacycgr  35333  imagesset  36135  meran1  36593  meran3  36595  mh-setind  36718  regsfromregtco  36720  regsfromunir1  36722  bj-modal4e  37014  f1omptsnlem  37652  mptsnunlem  37654  topdifinffinlem  37663  relowlpssretop  37680  poimirlem25  37966  eqbrb  38560  eqelb  38562  symrefref3  38969  dedths  39408  sn-axrep5v  42658  dffltz  43067  mzpincl  43166  lerabdioph  43233  ltrabdioph  43236  nerabdioph  43237  dvdsrabdioph  43238  finona1cl  43880  frege91  44381  frege97  44387  frege98  44388  frege109  44399  sumnnodd  46060  limsupvaluz2  46166  aiotaval  47543  rrx2linest  49218  fonex  49342