Theorem 3imtr3i 283

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  rb-ax1  1716  speimfwALT  1926  cbv1  2336  hblem  2889  nfcrii  2918  axrep1  5046  tfinds2  7392  smores  7791  idssen  8349  1sdom  8514  itunitc1  9638  dominf  9663  dominfac  9791  ssxr  10508  nnwos  12127  pmatcollpw3lem  21110  ppttop  21334  ptclsg  21942  sincosq3sgn  24804  adjbdln  29656  fmptdF  30180  funcnv4mpt  30193  disjdsct  30214  esumpcvgval  31013  esumcvg  31021  measiuns  31153  ballotlemodife  31433  bnj605  31858  bnj594  31863  imagesset  32972  meran1  33316  meran3  33318  bj-modal4e  33595  bj-cbv1v  33613  bj-axrep1  33655  f1omptsnlem  34096  mptsnunlem  34098  topdifinffinlem  34107  relowlpssretop  34124  poimirlem25  34395  eqelb  34983  symrefref3  35282  dedths  35580  sn-axrep5v  38590  dffltz  38716  mzpincl  38764  lerabdioph  38836  ltrabdioph  38839  nerabdioph  38840  dvdsrabdioph  38841  frege91  39701  frege97  39707  frege98  39708  frege109  39719  sumnnodd  41376  aiotaval  42733  rrx2linest  44131