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  1752  speimfwALT  1964  cbv1v  2334  cbv1  2400  hblem  2859  hblemg  2860  sbhypf  3510  axrep1  5235  axrep4v  5239  axrep4  5240  tfinds2  7840  smores  8321  idssen  8968  1sdomOLD  9196  ssttrcl  9668  itunitc1  10373  dominf  10398  dominfac  10526  ssxr  11243  nnwos  12874  pmatcollpw3lem  22670  ppttop  22894  ptclsg  23502  sincosq3sgn  26409  adjbdln  32012  fmptdF  32580  funcnv4mpt  32593  disjdsct  32626  esumpcvgval  34068  esumcvg  34076  measiuns  34207  ballotlemodife  34489  bnj605  34897  bnj594  34902  acycgr0v  35135  prclisacycgr  35138  imagesset  35941  meran1  36399  meran3  36401  bj-modal4e  36703  f1omptsnlem  37324  mptsnunlem  37326  topdifinffinlem  37335  relowlpssretop  37352  poimirlem25  37639  eqbrb  38221  eqelb  38223  symrefref3  38555  dedths  38955  sn-axrep5v  42204  dffltz  42622  mzpincl  42722  lerabdioph  42793  ltrabdioph  42796  nerabdioph  42797  dvdsrabdioph  42798  finona1cl  43442  frege91  43943  frege97  43949  frege98  43950  frege109  43961  sumnnodd  45628  limsupvaluz2  45736  aiotaval  47096  rrx2linest  48731  fonex  48855