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  842  stdcn  847  dcan  933  xordc1  1393  hbxfrbi  1472  nfalt  1578  19.29r  1621  19.31r  1681  sbimi  1764  spsbbi  1844  sbi2v  1892  euan  2082  2exeu  2118  ralimi2  2537  reximi2  2573  r19.28av  2613  r19.29r  2615  elex  2749  rmoan  2938  rmoimi2  2941  sseq2  3180  rabss2  3239  unssdif  3371  inssdif  3372  unssin  3375  inssun  3376  rabn0r  3450  undif4  3486  ssdif0im  3488  inssdif0im  3491  ssundifim  3507  ralf0  3527  prmg  3714  difprsnss  3731  snsspw  3765  pwprss  3806  pwtpss  3807  uniin  3830  intss  3866  iuniin  3897  iuneq1  3900  iuneq2  3903  iundif2ss  3953  iinuniss  3970  iunpwss  3979  intexrabim  4154  exmidundif  4207  exmidundifim  4208  exss  4228  pwunss  4284  soeq2  4317  ordunisuc2r  4514  peano5  4598  reliin  4749  coeq1  4785  coeq2  4786  cnveq  4802  dmeq  4828  dmin  4836  dmcoss  4897  rncoeq  4901  resiexg  4953  dminss  5044  imainss  5045  dfco2a  5130  euiotaex  5195  eliotaeu  5206  fununi  5285  fof  5439  f1ocnv  5475  rexrnmpt  5660  isocnv  5812  isotr  5817  oprabid  5907  dmtpos  6257  tposfn  6274  smores  6293  eqer  6567  ixpeq2  6712  enssdom  6762  fiprc  6815  fiintim  6928  ltexprlemlol  7601  ltexprlemupu  7603  recexgt0  8537  peano2uz2  9360  eluzp1p1  9553  peano2uz  9583  zq  9626  ubmelfzo  10200  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  expclzaplem  10544  hashfiv01gt1  10762  fsum2dlemstep  11442  fprod2dlemstep  11630  sin02gt0  11771  qredeu  12097  prmdc  12130  lgslem3  14406  bj-stim  14501  bj-stan  14502  bj-stal  14504  bj-nfalt  14519  bj-indint  14686  tridceq  14807