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  2367  cbv1  2433  hblem  2893  hblemg  2894  sbhypf  3512  axrep1  5237  axrep4v  5241  axrep4  5242  tfinds2  7864  smores  8345  idssen  9007  ssttrcl  9698  itunitc1  10426  dominf  10451  dominfac  10586  ssxr  11307  nnwos  12968  chnfibg  18730  pmatcollpw3lem  23014  ppttop  23238  ptclsg  23847  sincosq3sgn  26745  adjbdln  32572  fmptdf2  33137  funcnv4mpt  33149  disjdsct  33183  esumpcvgval  34596  esumcvg  34604  measiuns  34736  ballotlemodife  35017  bnj605  35424  bnj594  35429  axreg  35661  axregs  35673  acycgr0v  35735  prclisacycgr  35738  imagesset  36540  meran1  37038  meran3  37040  mh-setind  37163  regsfromregtco  37165  regsfromunir1  37167  bj-modal4e  37458  f1omptsnlem  38098  mptsnunlem  38100  topdifinffinlem  38109  relowlpssretop  38126  poimirlem25  38402  eqbrb  38995  eqelb  38997  symrefref3  39404  dedths  39843  sn-axrep5v  43095  dffltz  43488  mzpincl  43587  lerabdioph  43654  ltrabdioph  43657  nerabdioph  43658  dvdsrabdioph  43659  finona1cl  44301  frege91  44802  frege97  44808  frege98  44809  frege109  44820  sumnnodd  46468  limsupvaluz2  46574  aiotaval  47991  rrx2linest  49680  fonex  49803