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  847  stdcn  852  ifpdc  985  xordc1  1435  hbxfrbi  1518  nfalt  1624  19.29r  1667  19.31r  1727  sbimi  1810  spsbbi  1890  sbi2v  1939  euan  2134  2exeu  2170  ralimi2  2590  reximi2  2626  r19.28av  2667  r19.29r  2669  elex  2811  rmoan  3003  rmoimi2  3006  sseq2  3248  rabss2  3307  unssdif  3439  inssdif  3440  unssin  3443  inssun  3444  rabn0r  3518  undif4  3554  ssdif0im  3556  inssdif0im  3559  ssundifim  3575  ralf0  3594  prmg  3789  difprsnss  3806  snsspw  3842  pwprss  3884  pwtpss  3885  uniin  3908  intss  3944  iuniin  3975  iuneq1  3978  iuneq2  3981  iundif2ss  4031  iinuniss  4048  iunpwss  4057  intexrabim  4237  exmidundif  4290  exmidundifim  4291  exss  4313  pwunss  4374  soeq2  4407  ordunisuc2r  4606  peano5  4690  reliin  4841  coeq1  4879  coeq2  4880  cnveq  4896  dmeq  4923  dmin  4931  dmcoss  4994  rncoeq  4998  resiexg  5050  dminss  5143  imainss  5144  dfco2a  5229  euiotaex  5295  eliotaeu  5307  fundif  5365  fununi  5389  fof  5550  f1ocnv  5587  rexrnmpt  5780  isocnv  5941  isotr  5946  oprabid  6039  dmtpos  6408  tposfn  6425  smores  6444  eqer  6720  ixpeq2  6867  enssdom  6921  fiprc  6976  fiintim  7104  ltexprlemlol  7800  ltexprlemupu  7802  recexgt0  8738  peano2uz2  9565  eluzp1p1  9760  peano2uz  9790  zq  9833  ubmelfzo  10418  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  expclzaplem  10797  hashfiv01gt1  11016  wrdeq  11106  fsum2dlemstep  11960  fprod2dlemstep  12148  sin02gt0  12290  qredeu  12634  prmdc  12667  subrngrng  14181  lgslem3  15696  clwwlkccat  16138  bj-stim  16165  bj-stan  16166  bj-stal  16168  bj-nfalt  16183  bj-indint  16349  tridceq  16484