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  2336  cbv1  2402  hblem  2862  hblemg  2863  sbhypf  3498  axrep1  5216  axrep4v  5220  axrep4  5221  tfinds2  7794  smores  8272  idssen  8919  ssttrcl  9605  itunitc1  10311  dominf  10336  dominfac  10464  ssxr  11182  nnwos  12813  chnfibg  18542  pmatcollpw3lem  22698  ppttop  22922  ptclsg  23530  sincosq3sgn  26436  adjbdln  32063  fmptdF  32638  funcnv4mpt  32651  disjdsct  32684  esumpcvgval  34091  esumcvg  34099  measiuns  34230  ballotlemodife  34511  bnj605  34919  bnj594  34924  axreg  35125  axregs  35145  acycgr0v  35192  prclisacycgr  35195  imagesset  35997  meran1  36455  meran3  36457  bj-modal4e  36759  f1omptsnlem  37380  mptsnunlem  37382  topdifinffinlem  37391  relowlpssretop  37408  poimirlem25  37695  eqbrb  38284  eqelb  38286  symrefref3  38670  dedths  39071  sn-axrep5v  42319  dffltz  42737  mzpincl  42837  lerabdioph  42908  ltrabdioph  42911  nerabdioph  42912  dvdsrabdioph  42913  finona1cl  43556  frege91  44057  frege97  44063  frege98  44064  frege109  44075  sumnnodd  45740  limsupvaluz2  45846  aiotaval  47205  rrx2linest  48853  fonex  48977