Theorem 3imtr3i 294

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 238	. 2 ⊢ (𝜒 → 𝜓)
4		3imtr3.3	. 2 ⊢ (𝜓 ↔ 𝜃)
5	3, 4	sylib 221	1 ⊢ (𝜒 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  rb-ax1  1784  speimfwALT  1998  cbv1v  2368  cbv1  2434  hblem  2895  hblemg  2896  sbhypf  3513  axrep1  5236  axrep4v  5240  axrep4  5241  tfinds2  7885  smores  8374  idssen  9038  ssttrcl  9729  itunitc1  10511  dominf  10536  dominfac  10671  ssxr  11392  nnwos  13055  chnfibg  18825  pmatcollpw3lem  23116  ppttop  23340  ptclsg  23949  sincosq3sgn  26844  adjbdln  32700  fmptdf2  33307  funcnv4mpt  33319  disjdsct  33353  esumpcvgval  34766  esumcvg  34774  measiuns  34906  ballotlemodife  35186  bnj605  35593  bnj594  35598  axreg  35869  axregs  35881  acycgr0v  36027  prclisacycgr  36030  imagesset  36847  meran1  37329  meran3  37331  mh-setind  37454  regsfromregtco  37456  regsfromunir1  37458  bj-modal4e  37749  f1omptsnlem  38402  mptsnunlem  38404  topdifinffinlem  38413  relowlpssretop  38430  poimirlem25  38706  eqbrb  39314  eqelb  39316  symrefref3  39723  dedths  40162  sn-axrep5v  43414  dffltz  43813  mzpincl  43888  lerabdioph  43955  ltrabdioph  43958  nerabdioph  43959  dvdsrabdioph  43960  finona1cl  44597  frege91  45097  frege97  45103  frege98  45104  frege109  45115  sumnnodd  46784  limsupvaluz2  46890  aiotaval  48307  rrx2linest  49996  fonex  50120