Theorem 3imtr3i 290

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  1754  speimfwALT  1968  cbv1v  2332  cbv1  2400  hblem  2864  hblemg  2865  nfcriiOLD  2895  sbhypf  3508  axrep1  5248  tfinds2  7805  smores  8303  idssen  8944  1sdomOLD  9200  ssttrcl  9660  itunitc1  10365  dominf  10390  dominfac  10518  ssxr  11233  nnwos  12849  pmatcollpw3lem  22169  ppttop  22394  ptclsg  23003  sincosq3sgn  25894  adjbdln  31088  fmptdF  31639  funcnv4mpt  31652  disjdsct  31684  esumpcvgval  32766  esumcvg  32774  measiuns  32905  ballotlemodife  33186  bnj605  33608  bnj594  33613  acycgr0v  33829  prclisacycgr  33832  imagesset  34614  meran1  34959  meran3  34961  bj-modal4e  35256  f1omptsnlem  35880  mptsnunlem  35882  topdifinffinlem  35891  relowlpssretop  35908  poimirlem25  36176  eqbrb  36763  eqelb  36765  symrefref3  37099  dedths  37497  sn-axrep5v  40709  dffltz  41030  mzpincl  41115  lerabdioph  41186  ltrabdioph  41189  nerabdioph  41190  dvdsrabdioph  41191  finona1cl  41847  frege91  42348  frege97  42354  frege98  42355  frege109  42366  sumnnodd  43991  aiotaval  45447  rrx2linest  46948