Theorem 3imtr3i 294

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  rb-ax1  1779  speimfwALT  1991  cbv1v  2374  cbv1  2440  hblem  2900  hblemg  2901  sbhypf  3522  axrep1  5243  axrep4v  5247  axrep4  5248  tfinds2  7860  smores  8339  idssen  8994  ssttrcl  9684  itunitc1  10404  dominf  10429  dominfac  10558  ssxr  11279  nnwos  12939  chnfibg  18692  pmatcollpw3lem  22909  ppttop  23133  ptclsg  23741  sincosq3sgn  26631  adjbdln  32376  fmptdF  32942  funcnv4mpt  32954  disjdsct  32989  esumpcvgval  34413  esumcvg  34421  measiuns  34552  ballotlemodife  34833  bnj605  35240  bnj594  35245  axreg  35473  axregs  35485  acycgr0v  35573  prclisacycgr  35576  imagesset  36378  meran1  36845  meran3  36847  mh-setind  36970  regsfromregtco  36972  regsfromunir1  36974  bj-modal4e  37265  f1omptsnlem  37904  mptsnunlem  37906  topdifinffinlem  37915  relowlpssretop  37932  poimirlem25  38218  eqbrb  38812  eqelb  38814  symrefref3  39221  dedths  39660  sn-axrep5v  42912  dffltz  43292  mzpincl  43391  lerabdioph  43458  ltrabdioph  43461  nerabdioph  43462  dvdsrabdioph  43463  finona1cl  44105  frege91  44606  frege97  44612  frege98  44613  frege109  44624  sumnnodd  46272  limsupvaluz2  46378  aiotaval  47755  rrx2linest  49441  fonex  49564