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  854  stdcn  859  ifpdc  992  xordc1  1442  hbxfrbi  1525  nfalt  1631  19.29r  1674  19.31r  1733  sbimi  1817  spsbbi  1897  sbi2v  1947  euan  2143  2exeu  2179  ralimi2  2610  reximi2  2646  r19.28av  2687  r19.29r  2689  elex  2833  rmoan  3026  rmoimi2  3029  sseq2  3272  rabss2  3331  unssdif  3466  inssdif  3467  unssin  3470  inssun  3471  rabn0r  3548  undif4  3586  ssdif0im  3588  inssdif0im  3591  ssundifim  3608  ralf0  3627  prmg  3830  difprsnss  3848  snsspw  3884  pwprss  3926  pwtpss  3927  uniin  3950  intss  3986  iuniin  4017  iuneq1  4020  iuneq2  4023  iundif2ss  4073  iinuniss  4090  iunpwss  4099  intexrabim  4284  exmidundif  4338  exmidundifim  4339  exss  4362  pwunss  4423  soeq2  4456  ordunisuc2r  4656  peano5  4740  reliin  4894  coeq1  4932  coeq2  4933  cnveq  4949  dmeq  4976  dmin  4984  dmcoss  5047  rncoeq  5051  resiexg  5103  dminss  5197  imainss  5198  dfco2a  5283  euiotaex  5349  eliotaeu  5361  fundif  5420  fununi  5444  fof  5610  f1ocnv  5647  rexrnmpt  5842  isocnv  6007  isotr  6012  oprabid  6107  dmtpos  6517  tposfn  6534  smores  6553  eqer  6829  fsetsspwxp  6938  ixpeq2  6984  enssdom  7038  fiprc  7094  fiintim  7228  ltexprlemlol  7959  ltexprlemupu  7961  recexgt0  8898  peano2uz2  9732  eluzp1p1  9927  peano2uz  9962  zq  10005  ubmelfzo  10596  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  expclzaplem  10978  hashfiv01gt1  11199  hashfibclem  11260  wrdeq  11304  fsum2dlemstep  12179  fprod2dlemstep  12367  sin02gt0  12509  qredeu  12853  prmdc  12886  ballotfilemth  13259  subrngrng  14483  lgslem3  16035  clwwlkccat  16556  clwwlknonccat  16588  bj-stim  16688  bj-stan  16689  bj-stal  16691  bj-nfalt  16706  bj-indint  16871  tridceq  17011