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  1751  speimfwALT  1963  cbv1v  2337  cbv1  2406  hblem  2872  hblemg  2873  sbhypf  3543  axrep1  5279  axrep4v  5283  axrep4  5284  tfinds2  7886  smores  8393  idssen  9038  1sdomOLD  9286  ssttrcl  9756  itunitc1  10461  dominf  10486  dominfac  10614  ssxr  11331  nnwos  12958  pmatcollpw3lem  22790  ppttop  23015  ptclsg  23624  sincosq3sgn  26543  adjbdln  32103  fmptdF  32667  funcnv4mpt  32680  disjdsct  32713  esumpcvgval  34080  esumcvg  34088  measiuns  34219  ballotlemodife  34501  bnj605  34922  bnj594  34927  acycgr0v  35154  prclisacycgr  35157  imagesset  35955  meran1  36413  meran3  36415  bj-modal4e  36717  f1omptsnlem  37338  mptsnunlem  37340  topdifinffinlem  37349  relowlpssretop  37366  poimirlem25  37653  eqbrb  38235  eqelb  38237  symrefref3  38566  dedths  38964  sn-axrep5v  42256  dffltz  42649  mzpincl  42750  lerabdioph  42821  ltrabdioph  42824  nerabdioph  42825  dvdsrabdioph  42826  finona1cl  43471  frege91  43972  frege97  43978  frege98  43979  frege109  43990  sumnnodd  45650  limsupvaluz2  45758  aiotaval  47112  rrx2linest  48668  fonex  48774