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  2366  cbv1  2432  hblem  2892  hblemg  2893  sbhypf  3510  axrep1  5233  axrep4v  5237  axrep4  5238  tfinds2  7875  smores  8360  idssen  9024  ssttrcl  9716  itunitc1  10498  dominf  10523  dominfac  10658  ssxr  11379  nnwos  13042  chnfibg  18810  pmatcollpw3lem  23101  ppttop  23325  ptclsg  23934  sincosq3sgn  26829  adjbdln  32685  fmptdf2  33250  funcnv4mpt  33262  disjdsct  33296  esumpcvgval  34710  esumcvg  34718  measiuns  34850  ballotlemodife  35130  bnj605  35537  bnj594  35542  axreg  35795  axregs  35807  acycgr0v  35913  prclisacycgr  35916  imagesset  36717  meran1  37199  meran3  37201  mh-setind  37324  regsfromregtco  37326  regsfromunir1  37328  bj-modal4e  37619  f1omptsnlem  38259  mptsnunlem  38261  topdifinffinlem  38270  relowlpssretop  38287  poimirlem25  38563  eqbrb  39171  eqelb  39173  symrefref3  39580  dedths  40019  sn-axrep5v  43271  dffltz  43670  mzpincl  43744  lerabdioph  43811  ltrabdioph  43814  nerabdioph  43815  dvdsrabdioph  43816  finona1cl  44453  frege91  44953  frege97  44959  frege98  44960  frege109  44971  sumnnodd  46641  limsupvaluz2  46747  aiotaval  48164  rrx2linest  49853  fonex  49976