Theorem 3imtr3i 292

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  rb-ax1  1759  speimfwALT  1971  cbv1v  2344  cbv1  2410  hblem  2870  hblemg  2871  sbhypf  3491  axrep1  5201  axrep4v  5205  axrep4  5206  tfinds2  7805  smores  8283  idssen  8935  ssttrcl  9628  itunitc1  10334  dominf  10359  dominfac  10488  ssxr  11207  nnwos  12857  chnfibg  18594  pmatcollpw3lem  22767  ppttop  22991  ptclsg  23599  sincosq3sgn  26483  adjbdln  32173  fmptdF  32749  funcnv4mpt  32761  disjdsct  32796  esumpcvgval  34271  esumcvg  34279  measiuns  34410  ballotlemodife  34691  bnj605  35098  bnj594  35103  axreg  35317  axregs  35329  acycgr0v  35385  prclisacycgr  35388  imagesset  36190  meran1  36648  meran3  36650  mh-setind  36773  regsfromregtco  36775  regsfromunir1  36777  bj-modal4e  37069  f1omptsnlem  37707  mptsnunlem  37709  topdifinffinlem  37718  relowlpssretop  37735  poimirlem25  38021  eqbrb  38615  eqelb  38617  symrefref3  39024  dedths  39463  sn-axrep5v  42713  dffltz  43093  mzpincl  43192  lerabdioph  43259  ltrabdioph  43262  nerabdioph  43263  dvdsrabdioph  43264  finona1cl  43906  frege91  44407  frege97  44413  frege98  44414  frege109  44425  sumnnodd  46083  limsupvaluz2  46189  aiotaval  47566  rrx2linest  49241  fonex  49365