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  1785  speimfwALT  1997  cbv1v  2365  cbv1  2431  hblem  2891  hblemg  2892  sbhypf  3509  axrep1  5233  axrep4v  5237  axrep4  5238  tfinds2  7861  smores  8342  idssen  9006  ssttrcl  9697  itunitc1  10425  dominf  10450  dominfac  10585  ssxr  11306  nnwos  12967  chnfibg  18727  pmatcollpw3lem  23011  ppttop  23235  ptclsg  23844  sincosq3sgn  26741  adjbdln  32567  fmptdf2  33132  funcnv4mpt  33144  disjdsct  33178  esumpcvgval  34591  esumcvg  34599  measiuns  34731  ballotlemodife  35012  bnj605  35419  bnj594  35424  axreg  35656  axregs  35668  acycgr0v  35730  prclisacycgr  35733  imagesset  36535  meran1  37033  meran3  37035  mh-setind  37158  regsfromregtco  37160  regsfromunir1  37162  bj-modal4e  37453  f1omptsnlem  38093  mptsnunlem  38095  topdifinffinlem  38104  relowlpssretop  38121  poimirlem25  38397  eqbrb  38990  eqelb  38992  symrefref3  39399  dedths  39838  sn-axrep5v  43090  dffltz  43483  mzpincl  43582  lerabdioph  43649  ltrabdioph  43652  nerabdioph  43653  dvdsrabdioph  43654  finona1cl  44296  frege91  44797  frege97  44803  frege98  44804  frege109  44815  sumnnodd  46463  limsupvaluz2  46569  aiotaval  47986  rrx2linest  49675  fonex  49798