Theorem 3imtr3i 291

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  2331  cbv1  2400  hblem  2868  hblemg  2869  nfcriiOLD  2898  axrep1  5219  tfinds2  7742  smores  8214  idssen  8818  1sdomOLD  9070  ssttrcl  9517  itunitc1  10222  dominf  10247  dominfac  10375  ssxr  11090  nnwos  12701  pmatcollpw3lem  21977  ppttop  22202  ptclsg  22811  sincosq3sgn  25702  adjbdln  30490  fmptdF  31038  funcnv4mpt  31051  disjdsct  31080  esumpcvgval  32091  esumcvg  32099  measiuns  32230  ballotlemodife  32509  bnj605  32932  bnj594  32937  acycgr0v  33155  prclisacycgr  33158  xpord3ind  33845  imagesset  34300  meran1  34645  meran3  34647  bj-modal4e  34942  f1omptsnlem  35551  mptsnunlem  35553  topdifinffinlem  35562  relowlpssretop  35579  poimirlem25  35846  eqelb  36426  symrefref3  36720  dedths  37018  sn-axrep5v  40227  dffltz  40508  mzpincl  40593  lerabdioph  40664  ltrabdioph  40667  nerabdioph  40668  dvdsrabdioph  40669  finona1cl  41098  frege91  41600  frege97  41606  frege98  41607  frege109  41618  sumnnodd  43220  aiotaval  44645  rrx2linest  46146