Theorem 3imtr4i 201

Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3imtr4.1	⊢ (𝜑 → 𝜓)
3imtr4.2	⊢ (𝜒 ↔ 𝜑)
3imtr4.3	⊢ (𝜃 ↔ 𝜓)

Assertion

Ref	Expression
3imtr4i	⊢ (𝜒 → 𝜃)

Proof of Theorem 3imtr4i

Step	Hyp	Ref	Expression
1		3imtr4.2	. . 3 ⊢ (𝜒 ↔ 𝜑)
2		3imtr4.1	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	sylbi 121	. 2 ⊢ (𝜒 → 𝜓)
4		3imtr4.3	. 2 ⊢ (𝜃 ↔ 𝜓)
5	3, 4	sylibr 134	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  dcn  843  stdcn  848  xordc1  1412  hbxfrbi  1494  nfalt  1600  19.29r  1643  19.31r  1703  sbimi  1786  spsbbi  1866  sbi2v  1915  euan  2109  2exeu  2145  ralimi2  2565  reximi2  2601  r19.28av  2641  r19.29r  2643  elex  2782  rmoan  2972  rmoimi2  2975  sseq2  3216  rabss2  3275  unssdif  3407  inssdif  3408  unssin  3411  inssun  3412  rabn0r  3486  undif4  3522  ssdif0im  3524  inssdif0im  3527  ssundifim  3543  ralf0  3562  prmg  3753  difprsnss  3770  snsspw  3804  pwprss  3845  pwtpss  3846  uniin  3869  intss  3905  iuniin  3936  iuneq1  3939  iuneq2  3942  iundif2ss  3992  iinuniss  4009  iunpwss  4018  intexrabim  4196  exmidundif  4249  exmidundifim  4250  exss  4270  pwunss  4329  soeq2  4362  ordunisuc2r  4561  peano5  4645  reliin  4796  coeq1  4834  coeq2  4835  cnveq  4851  dmeq  4877  dmin  4885  dmcoss  4947  rncoeq  4951  resiexg  5003  dminss  5096  imainss  5097  dfco2a  5182  euiotaex  5247  eliotaeu  5259  fundif  5317  fununi  5341  fof  5497  f1ocnv  5534  rexrnmpt  5722  isocnv  5879  isotr  5884  oprabid  5975  dmtpos  6341  tposfn  6358  smores  6377  eqer  6651  ixpeq2  6798  enssdom  6852  fiprc  6906  fiintim  7027  ltexprlemlol  7714  ltexprlemupu  7716  recexgt0  8652  peano2uz2  9479  eluzp1p1  9673  peano2uz  9703  zq  9746  ubmelfzo  10327  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  expclzaplem  10706  hashfiv01gt1  10925  wrdeq  11014  fsum2dlemstep  11687  fprod2dlemstep  11875  sin02gt0  12017  qredeu  12361  prmdc  12394  subrngrng  13906  lgslem3  15421  bj-stim  15615  bj-stan  15616  bj-stal  15618  bj-nfalt  15633  bj-indint  15800  tridceq  15928