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  3507  axrep1  5230  axrep4v  5234  axrep4  5235  tfinds2  7820  smores  8298  idssen  8945  1sdomOLD  9172  ssttrcl  9644  itunitc1  10349  dominf  10374  dominfac  10502  ssxr  11219  nnwos  12850  pmatcollpw3lem  22703  ppttop  22927  ptclsg  23535  sincosq3sgn  26442  adjbdln  32062  fmptdF  32630  funcnv4mpt  32643  disjdsct  32676  esumpcvgval  34061  esumcvg  34069  measiuns  34200  ballotlemodife  34482  bnj605  34890  bnj594  34895  acycgr0v  35128  prclisacycgr  35131  imagesset  35934  meran1  36392  meran3  36394  bj-modal4e  36696  f1omptsnlem  37317  mptsnunlem  37319  topdifinffinlem  37328  relowlpssretop  37345  poimirlem25  37632  eqbrb  38214  eqelb  38216  symrefref3  38548  dedths  38948  sn-axrep5v  42197  dffltz  42615  mzpincl  42715  lerabdioph  42786  ltrabdioph  42789  nerabdioph  42790  dvdsrabdioph  42791  finona1cl  43435  frege91  43936  frege97  43942  frege98  43943  frege109  43954  sumnnodd  45621  limsupvaluz2  45729  aiotaval  47089  rrx2linest  48724  fonex  48848