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  2338  cbv1  2407  hblem  2867  hblemg  2868  sbhypf  3528  axrep1  5255  axrep4v  5259  axrep4  5260  tfinds2  7864  smores  8371  idssen  9016  1sdomOLD  9262  ssttrcl  9734  itunitc1  10439  dominf  10464  dominfac  10592  ssxr  11309  nnwos  12936  pmatcollpw3lem  22726  ppttop  22950  ptclsg  23558  sincosq3sgn  26466  adjbdln  32069  fmptdF  32639  funcnv4mpt  32652  disjdsct  32685  esumpcvgval  34114  esumcvg  34122  measiuns  34253  ballotlemodife  34535  bnj605  34943  bnj594  34948  acycgr0v  35175  prclisacycgr  35178  imagesset  35976  meran1  36434  meran3  36436  bj-modal4e  36738  f1omptsnlem  37359  mptsnunlem  37361  topdifinffinlem  37370  relowlpssretop  37387  poimirlem25  37674  eqbrb  38256  eqelb  38258  symrefref3  38587  dedths  38985  sn-axrep5v  42234  dffltz  42632  mzpincl  42732  lerabdioph  42803  ltrabdioph  42806  nerabdioph  42807  dvdsrabdioph  42808  finona1cl  43452  frege91  43953  frege97  43959  frege98  43960  frege109  43971  sumnnodd  45639  limsupvaluz2  45747  aiotaval  47104  rrx2linest  48702  fonex  48822