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  844  stdcn  849  xordc1  1413  hbxfrbi  1496  nfalt  1602  19.29r  1645  19.31r  1705  sbimi  1788  spsbbi  1868  sbi2v  1917  euan  2111  2exeu  2147  ralimi2  2567  reximi2  2603  r19.28av  2643  r19.29r  2645  elex  2785  rmoan  2977  rmoimi2  2980  sseq2  3221  rabss2  3280  unssdif  3412  inssdif  3413  unssin  3416  inssun  3417  rabn0r  3491  undif4  3527  ssdif0im  3529  inssdif0im  3532  ssundifim  3548  ralf0  3567  prmg  3760  difprsnss  3777  snsspw  3813  pwprss  3855  pwtpss  3856  uniin  3879  intss  3915  iuniin  3946  iuneq1  3949  iuneq2  3952  iundif2ss  4002  iinuniss  4019  iunpwss  4028  intexrabim  4208  exmidundif  4261  exmidundifim  4262  exss  4284  pwunss  4343  soeq2  4376  ordunisuc2r  4575  peano5  4659  reliin  4810  coeq1  4848  coeq2  4849  cnveq  4865  dmeq  4892  dmin  4900  dmcoss  4962  rncoeq  4966  resiexg  5018  dminss  5111  imainss  5112  dfco2a  5197  euiotaex  5262  eliotaeu  5274  fundif  5332  fununi  5356  fof  5515  f1ocnv  5552  rexrnmpt  5741  isocnv  5898  isotr  5903  oprabid  5994  dmtpos  6360  tposfn  6377  smores  6396  eqer  6670  ixpeq2  6817  enssdom  6871  fiprc  6926  fiintim  7049  ltexprlemlol  7745  ltexprlemupu  7747  recexgt0  8683  peano2uz2  9510  eluzp1p1  9704  peano2uz  9734  zq  9777  ubmelfzo  10361  frecuzrdgtcl  10589  frecuzrdgfunlem  10596  expclzaplem  10740  hashfiv01gt1  10959  wrdeq  11048  fsum2dlemstep  11830  fprod2dlemstep  12018  sin02gt0  12160  qredeu  12504  prmdc  12537  subrngrng  14049  lgslem3  15564  bj-stim  15852  bj-stan  15853  bj-stal  15855  bj-nfalt  15870  bj-indint  16036  tridceq  16167