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  1773  speimfwALT  1985  cbv1v  2368  cbv1  2434  hblem  2894  hblemg  2895  sbhypf  3514  axrep1  5229  axrep4v  5233  axrep4  5234  tfinds2  7845  smores  8324  idssen  8979  ssttrcl  9671  itunitc1  10378  dominf  10403  dominfac  10532  ssxr  11253  nnwos  12917  chnfibg  18669  pmatcollpw3lem  22844  ppttop  23068  ptclsg  23676  sincosq3sgn  26566  adjbdln  32287  fmptdF  32859  funcnv4mpt  32871  disjdsct  32906  esumpcvgval  34376  esumcvg  34384  measiuns  34515  ballotlemodife  34796  bnj605  35203  bnj594  35208  axreg  35424  axregs  35436  acycgr0v  35499  prclisacycgr  35502  imagesset  36304  meran1  36772  meran3  36774  mh-setind  36897  regsfromregtco  36899  regsfromunir1  36901  bj-modal4e  37193  f1omptsnlem  37831  mptsnunlem  37833  topdifinffinlem  37842  relowlpssretop  37859  poimirlem25  38145  eqbrb  38739  eqelb  38741  symrefref3  39148  dedths  39587  sn-axrep5v  42837  dffltz  43217  mzpincl  43316  lerabdioph  43383  ltrabdioph  43386  nerabdioph  43387  dvdsrabdioph  43388  finona1cl  44030  frege91  44531  frege97  44537  frege98  44538  frege109  44549  sumnnodd  46207  limsupvaluz2  46313  aiotaval  47690  rrx2linest  49365  fonex  49489