Theorem 3imtr3i 291

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 235	. 2 ⊢ (𝜒 → 𝜓)
4		3imtr3.3	. 2 ⊢ (𝜓 ↔ 𝜃)
5	3, 4	sylib 218	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  rb-ax1  1750  speimfwALT  1964  cbv1v  2342  cbv1  2410  hblem  2876  hblemg  2877  sbhypf  3556  axrep1  5304  tfinds2  7901  smores  8408  idssen  9057  1sdomOLD  9312  ssttrcl  9784  itunitc1  10489  dominf  10514  dominfac  10642  ssxr  11359  nnwos  12980  pmatcollpw3lem  22810  ppttop  23035  ptclsg  23644  sincosq3sgn  26560  adjbdln  32115  fmptdF  32674  funcnv4mpt  32687  disjdsct  32714  esumpcvgval  34042  esumcvg  34050  measiuns  34181  ballotlemodife  34462  bnj605  34883  bnj594  34888  acycgr0v  35116  prclisacycgr  35119  imagesset  35917  meran1  36377  meran3  36379  bj-modal4e  36681  f1omptsnlem  37302  mptsnunlem  37304  topdifinffinlem  37313  relowlpssretop  37330  poimirlem25  37605  eqbrb  38188  eqelb  38190  symrefref3  38520  dedths  38918  sn-axrep5v  42209  dffltz  42589  mzpincl  42690  lerabdioph  42761  ltrabdioph  42764  nerabdioph  42765  dvdsrabdioph  42766  finona1cl  43415  frege91  43916  frege97  43922  frege98  43923  frege109  43934  sumnnodd  45551  aiotaval  47010  rrx2linest  48476