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  2338  cbv1  2404  hblem  2865  hblemg  2866  sbhypf  3500  axrep1  5223  axrep4v  5227  axrep4  5228  tfinds2  7804  smores  8282  idssen  8932  ssttrcl  9622  itunitc1  10328  dominf  10353  dominfac  10482  ssxr  11200  nnwos  12826  chnfibg  18557  pmatcollpw3lem  22725  ppttop  22949  ptclsg  23557  sincosq3sgn  26463  adjbdln  32107  fmptdF  32683  funcnv4mpt  32696  disjdsct  32731  esumpcvgval  34184  esumcvg  34192  measiuns  34323  ballotlemodife  34604  bnj605  35012  bnj594  35017  axreg  35232  axregs  35244  acycgr0v  35291  prclisacycgr  35294  imagesset  36096  meran1  36554  meran3  36556  bj-modal4e  36859  f1omptsnlem  37480  mptsnunlem  37482  topdifinffinlem  37491  relowlpssretop  37508  poimirlem25  37785  eqbrb  38374  eqelb  38376  symrefref3  38760  dedths  39161  sn-axrep5v  42414  dffltz  42819  mzpincl  42918  lerabdioph  42989  ltrabdioph  42992  nerabdioph  42993  dvdsrabdioph  42994  finona1cl  43636  frege91  44137  frege97  44143  frege98  44144  frege109  44155  sumnnodd  45818  limsupvaluz2  45924  aiotaval  47283  rrx2linest  48930  fonex  49054