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  850  stdcn  855  ifpdc  988  xordc1  1438  hbxfrbi  1521  nfalt  1627  19.29r  1670  19.31r  1729  sbimi  1812  spsbbi  1892  sbi2v  1941  euan  2136  2exeu  2172  ralimi2  2593  reximi2  2629  r19.28av  2670  r19.29r  2672  elex  2815  rmoan  3007  rmoimi2  3010  sseq2  3252  rabss2  3311  unssdif  3444  inssdif  3445  unssin  3448  inssun  3449  rabn0r  3523  undif4  3559  ssdif0im  3561  inssdif0im  3564  ssundifim  3580  ralf0  3599  prmg  3798  difprsnss  3816  snsspw  3852  pwprss  3894  pwtpss  3895  uniin  3918  intss  3954  iuniin  3985  iuneq1  3988  iuneq2  3991  iundif2ss  4041  iinuniss  4058  iunpwss  4067  intexrabim  4248  exmidundif  4302  exmidundifim  4303  exss  4325  pwunss  4386  soeq2  4419  ordunisuc2r  4618  peano5  4702  reliin  4855  coeq1  4893  coeq2  4894  cnveq  4910  dmeq  4937  dmin  4945  dmcoss  5008  rncoeq  5012  resiexg  5064  dminss  5158  imainss  5159  dfco2a  5244  euiotaex  5310  eliotaeu  5322  fundif  5381  fununi  5405  fof  5568  f1ocnv  5605  rexrnmpt  5798  isocnv  5962  isotr  5967  oprabid  6060  dmtpos  6465  tposfn  6482  smores  6501  eqer  6777  ixpeq2  6924  enssdom  6978  fiprc  7033  fiintim  7166  ltexprlemlol  7865  ltexprlemupu  7867  recexgt0  8802  peano2uz2  9631  eluzp1p1  9826  peano2uz  9861  zq  9904  ubmelfzo  10491  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  expclzaplem  10871  hashfiv01gt1  11090  wrdeq  11184  fsum2dlemstep  12058  fprod2dlemstep  12246  sin02gt0  12388  qredeu  12732  prmdc  12765  subrngrng  14280  lgslem3  15804  clwwlkccat  16325  clwwlknonccat  16357  bj-stim  16447  bj-stan  16448  bj-stal  16450  bj-nfalt  16465  bj-indint  16630  tridceq  16772