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  1813  spsbbi  1893  sbi2v  1943  euan  2139  2exeu  2175  ralimi2  2604  reximi2  2640  r19.28av  2681  r19.29r  2683  elex  2827  rmoan  3020  rmoimi2  3023  sseq2  3266  rabss2  3325  unssdif  3460  inssdif  3461  unssin  3464  inssun  3465  rabn0r  3539  undif4  3576  ssdif0im  3578  inssdif0im  3581  ssundifim  3598  ralf0  3617  prmg  3820  difprsnss  3838  snsspw  3874  pwprss  3916  pwtpss  3917  uniin  3940  intss  3976  iuniin  4007  iuneq1  4010  iuneq2  4013  iundif2ss  4063  iinuniss  4080  iunpwss  4089  intexrabim  4271  exmidundif  4325  exmidundifim  4326  exss  4349  pwunss  4410  soeq2  4443  ordunisuc2r  4643  peano5  4727  reliin  4881  coeq1  4919  coeq2  4920  cnveq  4936  dmeq  4963  dmin  4971  dmcoss  5034  rncoeq  5038  resiexg  5090  dminss  5184  imainss  5185  dfco2a  5270  euiotaex  5336  eliotaeu  5348  fundif  5407  fununi  5431  fof  5597  f1ocnv  5634  rexrnmpt  5827  isocnv  5992  isotr  5997  oprabid  6092  dmtpos  6502  tposfn  6519  smores  6538  eqer  6814  ixpeq2  6962  enssdom  7016  fiprc  7072  fiintim  7206  ltexprlemlol  7935  ltexprlemupu  7937  recexgt0  8874  peano2uz2  9708  eluzp1p1  9903  peano2uz  9938  zq  9981  ubmelfzo  10572  frecuzrdgtcl  10803  frecuzrdgfunlem  10810  expclzaplem  10954  hashfiv01gt1  11175  hashfibclem  11236  wrdeq  11276  fsum2dlemstep  12151  fprod2dlemstep  12339  sin02gt0  12481  qredeu  12825  prmdc  12858  ballotfilemth  13231  subrngrng  14455  lgslem3  16007  clwwlkccat  16528  clwwlknonccat  16560  bj-stim  16660  bj-stan  16661  bj-stal  16663  bj-nfalt  16678  bj-indint  16843  tridceq  16983