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  1942  euan  2137  2exeu  2173  ralimi2  2602  reximi2  2638  r19.28av  2679  r19.29r  2681  elex  2825  rmoan  3017  rmoimi2  3020  sseq2  3262  rabss2  3321  unssdif  3456  inssdif  3457  unssin  3460  inssun  3461  rabn0r  3535  undif4  3571  ssdif0im  3573  inssdif0im  3576  ssundifim  3593  ralf0  3612  prmg  3814  difprsnss  3832  snsspw  3868  pwprss  3910  pwtpss  3911  uniin  3934  intss  3970  iuniin  4001  iuneq1  4004  iuneq2  4007  iundif2ss  4057  iinuniss  4074  iunpwss  4083  intexrabim  4265  exmidundif  4319  exmidundifim  4320  exss  4343  pwunss  4404  soeq2  4437  ordunisuc2r  4636  peano5  4720  reliin  4874  coeq1  4912  coeq2  4913  cnveq  4929  dmeq  4956  dmin  4964  dmcoss  5027  rncoeq  5031  resiexg  5083  dminss  5177  imainss  5178  dfco2a  5263  euiotaex  5329  eliotaeu  5341  fundif  5400  fununi  5424  fof  5590  f1ocnv  5627  rexrnmpt  5820  isocnv  5984  isotr  5989  oprabid  6082  dmtpos  6487  tposfn  6504  smores  6523  eqer  6799  ixpeq2  6947  enssdom  7001  fiprc  7057  fiintim  7191  ltexprlemlol  7917  ltexprlemupu  7919  recexgt0  8854  peano2uz2  9685  eluzp1p1  9880  peano2uz  9915  zq  9958  ubmelfzo  10545  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  expclzaplem  10925  hashfiv01gt1  11145  hashfibclem  11206  wrdeq  11246  fsum2dlemstep  12120  fprod2dlemstep  12308  sin02gt0  12450  qredeu  12794  prmdc  12827  subrngrng  14347  lgslem3  15875  clwwlkccat  16396  clwwlknonccat  16428  bj-stim  16518  bj-stan  16519  bj-stal  16521  bj-nfalt  16536  bj-indint  16701  tridceq  16841