Theorem 3imtr3i 279

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  rb-ax1  1668  speimfwALT  1864  cbv1  2255  hblem  2718  axrep1  4700  tfinds2  6955  smores  7336  idssen  7886  1sdom  8048  itunitc1  9125  dominf  9150  dominfac  9274  ssxr  9986  nnwos  11631  pmatcollpw3lem  20407  ppttop  20621  ptclsg  21228  sincosq3sgn  24056  adjbdln  28326  fmptdF  28836  funcnv4mpt  28853  disjdsct  28863  esumpcvgval  29467  esumcvg  29475  measiuns  29607  ballotlemodife  29886  bnj605  30231  bnj594  30236  imagesset  31230  meran1  31580  meran3  31582  bj-nalnaleximiOLD  31798  bj-modal4e  31892  bj-cbv1v  31916  bj-axrep1  31976  bj-hblem  32043  f1omptsnlem  32359  mptsnunlem  32361  topdifinffinlem  32371  relowlpssretop  32388  poimirlem25  32604  dedths  33266  mzpincl  36315  lerabdioph  36387  ltrabdioph  36390  nerabdioph  36391  dvdsrabdioph  36392  frege91  37268  frege97  37274  frege98  37275  frege109  37286  sumnnodd  38697