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  2370  cbv1  2436  hblem  2896  hblemg  2897  sbhypf  3516  axrep1  5241  axrep4v  5245  axrep4  5246  tfinds2  7866  smores  8345  idssen  9000  ssttrcl  9691  itunitc1  10419  dominf  10444  dominfac  10577  ssxr  11298  nnwos  12959  chnfibg  18718  pmatcollpw3lem  22994  ppttop  23218  ptclsg  23827  sincosq3sgn  26720  adjbdln  32510  fmptdf2  33076  funcnv4mpt  33088  disjdsct  33123  esumpcvgval  34536  esumcvg  34544  measiuns  34676  ballotlemodife  34957  bnj605  35364  bnj594  35369  axreg  35601  axregs  35613  acycgr0v  35681  prclisacycgr  35684  imagesset  36486  meran1  36983  meran3  36985  mh-setind  37108  regsfromregtco  37110  regsfromunir1  37112  bj-modal4e  37403  f1omptsnlem  38043  mptsnunlem  38045  topdifinffinlem  38054  relowlpssretop  38071  poimirlem25  38357  eqbrb  38950  eqelb  38952  symrefref3  39359  dedths  39798  sn-axrep5v  43050  dffltz  43443  mzpincl  43542  lerabdioph  43609  ltrabdioph  43612  nerabdioph  43613  dvdsrabdioph  43614  finona1cl  44256  frege91  44757  frege97  44763  frege98  44764  frege109  44775  sumnnodd  46423  limsupvaluz2  46529  aiotaval  47909  rrx2linest  49598  fonex  49721