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  3575  ssdif0im  3577  inssdif0im  3580  ssundifim  3597  ralf0  3616  prmg  3819  difprsnss  3837  snsspw  3873  pwprss  3915  pwtpss  3916  uniin  3939  intss  3975  iuniin  4006  iuneq1  4009  iuneq2  4012  iundif2ss  4062  iinuniss  4079  iunpwss  4088  intexrabim  4270  exmidundif  4324  exmidundifim  4325  exss  4348  pwunss  4409  soeq2  4442  ordunisuc2r  4641  peano5  4725  reliin  4879  coeq1  4917  coeq2  4918  cnveq  4934  dmeq  4961  dmin  4969  dmcoss  5032  rncoeq  5036  resiexg  5088  dminss  5182  imainss  5183  dfco2a  5268  euiotaex  5334  eliotaeu  5346  fundif  5405  fununi  5429  fof  5595  f1ocnv  5632  rexrnmpt  5825  isocnv  5990  isotr  5995  oprabid  6090  dmtpos  6500  tposfn  6517  smores  6536  eqer  6812  ixpeq2  6960  enssdom  7014  fiprc  7070  fiintim  7204  ltexprlemlol  7933  ltexprlemupu  7935  recexgt0  8871  peano2uz2  9703  eluzp1p1  9898  peano2uz  9933  zq  9976  ubmelfzo  10567  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  expclzaplem  10949  hashfiv01gt1  11170  hashfibclem  11231  wrdeq  11271  fsum2dlemstep  12145  fprod2dlemstep  12333  sin02gt0  12475  qredeu  12819  prmdc  12852  ballotfilemth  13225  subrngrng  14448  lgslem3  16001  clwwlkccat  16522  clwwlknonccat  16554  bj-stim  16644  bj-stan  16645  bj-stal  16647  bj-nfalt  16662  bj-indint  16827  tridceq  16967