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 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  rb-ax1  1782  speimfwALT  1994  cbv1v  2368  cbv1  2434  hblem  2894  hblemg  2895  sbhypf  3514  axrep1  5239  axrep4v  5243  axrep4  5244  tfinds2  7856  smores  8335  idssen  8990  ssttrcl  9680  itunitc1  10399  dominf  10424  dominfac  10553  ssxr  11274  nnwos  12934  chnfibg  18687  pmatcollpw3lem  22940  ppttop  23164  ptclsg  23772  sincosq3sgn  26665  adjbdln  32435  fmptdF  33001  funcnv4mpt  33013  disjdsct  33048  esumpcvgval  34468  esumcvg  34476  measiuns  34607  ballotlemodife  34888  bnj605  35295  bnj594  35300  axreg  35540  axregs  35552  acycgr0v  35640  prclisacycgr  35643  imagesset  36445  meran1  36942  meran3  36944  mh-setind  37067  regsfromregtco  37069  regsfromunir1  37071  bj-modal4e  37362  f1omptsnlem  38002  mptsnunlem  38004  topdifinffinlem  38013  relowlpssretop  38030  poimirlem25  38316  eqbrb  38908  eqelb  38910  symrefref3  39317  dedths  39756  sn-axrep5v  43008  dffltz  43386  mzpincl  43485  lerabdioph  43552  ltrabdioph  43555  nerabdioph  43556  dvdsrabdioph  43557  finona1cl  44199  frege91  44700  frege97  44706  frege98  44707  frege109  44718  sumnnodd  46366  limsupvaluz2  46472  aiotaval  47852  rrx2linest  49542  fonex  49665