Theorem 3imtr3i 293

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  rb-ax1  1753  speimfwALT  1967  cbv1v  2356  cbv1  2422  hblem  2943  hblemg  2944  nfcrii  2970  axrep1  5191  tfinds2  7578  smores  7989  idssen  8554  1sdom  8721  itunitc1  9842  dominf  9867  dominfac  9995  ssxr  10710  nnwos  12316  pmatcollpw3lem  21391  ppttop  21615  ptclsg  22223  sincosq3sgn  25086  adjbdln  29860  fmptdF  30401  funcnv4mpt  30414  disjdsct  30438  esumpcvgval  31337  esumcvg  31345  measiuns  31476  ballotlemodife  31755  bnj605  32179  bnj594  32184  acycgr0v  32395  prclisacycgr  32398  imagesset  33414  meran1  33759  meran3  33761  bj-modal4e  34049  f1omptsnlem  34620  mptsnunlem  34622  topdifinffinlem  34631  relowlpssretop  34648  poimirlem25  34932  eqelb  35517  symrefref3  35815  dedths  36113  sn-axrep5v  39128  dffltz  39291  mzpincl  39351  lerabdioph  39422  ltrabdioph  39425  nerabdioph  39426  dvdsrabdioph  39427  frege91  40320  frege97  40326  frege98  40327  frege109  40338  sumnnodd  41931  aiotaval  43313  rrx2linest  44749