Theorem 3imtr3i 290

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 234	. 2 ⊢ (𝜒 → 𝜓)
4		3imtr3.3	. 2 ⊢ (𝜓 ↔ 𝜃)
5	3, 4	sylib 217	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  rb-ax1  1758  speimfwALT  1971  cbv1v  2336  cbv1  2403  hblem  2871  hblemg  2872  nfcriiOLD  2901  axrep1  5214  tfinds2  7698  smores  8167  idssen  8756  1sdom  8987  ssttrcl  9434  itunitc1  10160  dominf  10185  dominfac  10313  ssxr  11028  nnwos  12637  pmatcollpw3lem  21913  ppttop  22138  ptclsg  22747  sincosq3sgn  25638  adjbdln  30424  fmptdF  30972  funcnv4mpt  30985  disjdsct  31014  esumpcvgval  32025  esumcvg  32033  measiuns  32164  ballotlemodife  32443  bnj605  32866  bnj594  32871  acycgr0v  33089  prclisacycgr  33092  xpord3ind  33779  imagesset  34234  meran1  34579  meran3  34581  bj-modal4e  34876  f1omptsnlem  35486  mptsnunlem  35488  topdifinffinlem  35497  relowlpssretop  35514  poimirlem25  35781  eqelb  36361  symrefref3  36657  dedths  36955  sn-axrep5v  40165  dffltz  40451  mzpincl  40536  lerabdioph  40607  ltrabdioph  40610  nerabdioph  40611  dvdsrabdioph  40612  frege91  41515  frege97  41521  frege98  41522  frege109  41533  sumnnodd  43125  aiotaval  44538  rrx2linest  46040