Theorem 3imtr3i 290

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  rb-ax1  1752  speimfwALT  1966  cbv1v  2330  cbv1  2399  hblem  2863  hblemg  2864  nfcriiOLD  2894  sbhypf  3537  axrep1  5285  tfinds2  7855  smores  8354  idssen  8995  1sdomOLD  9251  ssttrcl  9712  itunitc1  10417  dominf  10442  dominfac  10570  ssxr  11287  nnwos  12903  pmatcollpw3lem  22505  ppttop  22730  ptclsg  23339  sincosq3sgn  26246  adjbdln  31603  fmptdF  32148  funcnv4mpt  32161  disjdsct  32191  esumpcvgval  33374  esumcvg  33382  measiuns  33513  ballotlemodife  33794  bnj605  34216  bnj594  34221  acycgr0v  34437  prclisacycgr  34440  imagesset  35229  meran1  35599  meran3  35601  bj-modal4e  35896  f1omptsnlem  36520  mptsnunlem  36522  topdifinffinlem  36531  relowlpssretop  36548  poimirlem25  36816  eqbrb  37402  eqelb  37404  symrefref3  37737  dedths  38135  sn-axrep5v  41339  dffltz  41678  mzpincl  41774  lerabdioph  41845  ltrabdioph  41848  nerabdioph  41849  dvdsrabdioph  41850  finona1cl  42506  frege91  43007  frege97  43013  frege98  43014  frege109  43025  sumnnodd  44644  aiotaval  46101  rrx2linest  47515