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  849  stdcn  854  ifpdc  987  xordc1  1437  hbxfrbi  1520  nfalt  1626  19.29r  1669  19.31r  1729  sbimi  1812  spsbbi  1892  sbi2v  1941  euan  2136  2exeu  2172  ralimi2  2592  reximi2  2628  r19.28av  2669  r19.29r  2671  elex  2814  rmoan  3006  rmoimi2  3009  sseq2  3251  rabss2  3310  unssdif  3442  inssdif  3443  unssin  3446  inssun  3447  rabn0r  3521  undif4  3557  ssdif0im  3559  inssdif0im  3562  ssundifim  3578  ralf0  3597  prmg  3794  difprsnss  3811  snsspw  3847  pwprss  3889  pwtpss  3890  uniin  3913  intss  3949  iuniin  3980  iuneq1  3983  iuneq2  3986  iundif2ss  4036  iinuniss  4053  iunpwss  4062  intexrabim  4243  exmidundif  4296  exmidundifim  4297  exss  4319  pwunss  4380  soeq2  4413  ordunisuc2r  4612  peano5  4696  reliin  4849  coeq1  4887  coeq2  4888  cnveq  4904  dmeq  4931  dmin  4939  dmcoss  5002  rncoeq  5006  resiexg  5058  dminss  5151  imainss  5152  dfco2a  5237  euiotaex  5303  eliotaeu  5315  fundif  5374  fununi  5398  fof  5559  f1ocnv  5596  rexrnmpt  5790  isocnv  5951  isotr  5956  oprabid  6049  dmtpos  6421  tposfn  6438  smores  6457  eqer  6733  ixpeq2  6880  enssdom  6934  fiprc  6989  fiintim  7122  ltexprlemlol  7821  ltexprlemupu  7823  recexgt0  8759  peano2uz2  9586  eluzp1p1  9781  peano2uz  9816  zq  9859  ubmelfzo  10444  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  expclzaplem  10824  hashfiv01gt1  11043  wrdeq  11134  fsum2dlemstep  11994  fprod2dlemstep  12182  sin02gt0  12324  qredeu  12668  prmdc  12701  subrngrng  14215  lgslem3  15730  clwwlkccat  16251  clwwlknonccat  16283  bj-stim  16342  bj-stan  16343  bj-stal  16345  bj-nfalt  16360  bj-indint  16526  tridceq  16660