Theorem 3imtr3i 280

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  rb-ax1  1677  speimfwALT  1877  cbv1  2267  hblem  2731  axrep1  4772  tfinds2  7063  smores  7449  idssen  8000  1sdom  8163  itunitc1  9242  dominf  9267  dominfac  9395  ssxr  10107  nnwos  11755  pmatcollpw3lem  20588  ppttop  20811  ptclsg  21418  sincosq3sgn  24252  adjbdln  28942  fmptdF  29456  funcnv4mpt  29470  disjdsct  29480  esumpcvgval  30140  esumcvg  30148  measiuns  30280  ballotlemodife  30559  bnj605  30977  bnj594  30982  imagesset  32060  meran1  32410  meran3  32412  bj-modal4e  32705  bj-cbv1v  32729  bj-axrep1  32788  bj-hblem  32849  f1omptsnlem  33183  mptsnunlem  33185  topdifinffinlem  33195  relowlpssretop  33212  poimirlem25  33434  eqelb  34002  dedths  34248  mzpincl  37297  lerabdioph  37369  ltrabdioph  37372  nerabdioph  37373  dvdsrabdioph  37374  frege91  38248  frege97  38254  frege98  38255  frege109  38266  sumnnodd  39862