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  3491  axrep1  5214  axrep4v  5218  axrep4  5219  tfinds2  7810  smores  8287  idssen  8939  ssttrcl  9631  itunitc1  10337  dominf  10362  dominfac  10491  ssxr  11210  nnwos  12860  chnfibg  18597  pmatcollpw3lem  22762  ppttop  22986  ptclsg  23594  sincosq3sgn  26481  adjbdln  32173  fmptdF  32748  funcnv4mpt  32760  disjdsct  32795  esumpcvgval  34242  esumcvg  34250  measiuns  34381  ballotlemodife  34662  bnj605  35069  bnj594  35074  axreg  35291  axregs  35303  acycgr0v  35350  prclisacycgr  35353  imagesset  36155  meran1  36613  meran3  36615  mh-setind  36738  regsfromregtco  36740  regsfromunir1  36742  bj-modal4e  37034  f1omptsnlem  37670  mptsnunlem  37672  topdifinffinlem  37681  relowlpssretop  37698  poimirlem25  37984  eqbrb  38578  eqelb  38580  symrefref3  38987  dedths  39426  sn-axrep5v  42676  dffltz  43085  mzpincl  43184  lerabdioph  43255  ltrabdioph  43258  nerabdioph  43259  dvdsrabdioph  43260  finona1cl  43902  frege91  44403  frege97  44409  frege98  44410  frege109  44421  sumnnodd  46082  limsupvaluz2  46188  aiotaval  47559  rrx2linest  49234  fonex  49358