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  1749  speimfwALT  1962  cbv1v  2337  cbv1  2405  hblem  2871  hblemg  2872  sbhypf  3544  axrep1  5286  axrep4v  5290  axrep4  5291  tfinds2  7885  smores  8391  idssen  9036  1sdomOLD  9283  ssttrcl  9753  itunitc1  10458  dominf  10483  dominfac  10611  ssxr  11328  nnwos  12955  pmatcollpw3lem  22805  ppttop  23030  ptclsg  23639  sincosq3sgn  26557  adjbdln  32112  fmptdF  32673  funcnv4mpt  32686  disjdsct  32718  esumpcvgval  34059  esumcvg  34067  measiuns  34198  ballotlemodife  34479  bnj605  34900  bnj594  34905  acycgr0v  35133  prclisacycgr  35136  imagesset  35935  meran1  36394  meran3  36396  bj-modal4e  36698  f1omptsnlem  37319  mptsnunlem  37321  topdifinffinlem  37330  relowlpssretop  37347  poimirlem25  37632  eqbrb  38214  eqelb  38216  symrefref3  38546  dedths  38944  sn-axrep5v  42234  dffltz  42621  mzpincl  42722  lerabdioph  42793  ltrabdioph  42796  nerabdioph  42797  dvdsrabdioph  42798  finona1cl  43443  frege91  43944  frege97  43950  frege98  43951  frege109  43962  sumnnodd  45586  limsupvaluz2  45694  aiotaval  47045  rrx2linest  48592