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  842  stdcn  847  dcan  933  xordc1  1393  hbxfrbi  1470  nfalt  1576  19.29r  1619  19.31r  1679  sbimi  1762  spsbbi  1842  sbi2v  1890  euan  2080  2exeu  2116  ralimi2  2535  reximi2  2571  r19.28av  2611  r19.29r  2613  elex  2746  rmoan  2935  rmoimi2  2938  sseq2  3177  rabss2  3236  unssdif  3368  inssdif  3369  unssin  3372  inssun  3373  rabn0r  3447  undif4  3483  ssdif0im  3485  inssdif0im  3488  ssundifim  3504  ralf0  3524  prmg  3710  difprsnss  3727  snsspw  3760  pwprss  3801  pwtpss  3802  uniin  3825  intss  3861  iuniin  3892  iuneq1  3895  iuneq2  3898  iundif2ss  3947  iinuniss  3964  iunpwss  3973  intexrabim  4148  exmidundif  4201  exmidundifim  4202  exss  4221  pwunss  4277  soeq2  4310  ordunisuc2r  4507  peano5  4591  reliin  4742  coeq1  4777  coeq2  4778  cnveq  4794  dmeq  4820  dmin  4828  dmcoss  4889  rncoeq  4893  resiexg  4945  dminss  5035  imainss  5036  dfco2a  5121  euiotaex  5186  eliotaeu  5197  fununi  5276  fof  5430  f1ocnv  5466  rexrnmpt  5651  isocnv  5802  isotr  5807  oprabid  5897  dmtpos  6247  tposfn  6264  smores  6283  eqer  6557  ixpeq2  6702  enssdom  6752  fiprc  6805  fiintim  6918  ltexprlemlol  7576  ltexprlemupu  7578  recexgt0  8511  peano2uz2  9333  eluzp1p1  9526  peano2uz  9556  zq  9599  ubmelfzo  10170  frecuzrdgtcl  10382  frecuzrdgfunlem  10389  expclzaplem  10514  hashfiv01gt1  10730  fsum2dlemstep  11410  fprod2dlemstep  11598  sin02gt0  11739  qredeu  12064  prmdc  12097  lgslem3  13974  bj-stim  14058  bj-stan  14059  bj-stal  14061  bj-nfalt  14076  bj-indint  14243  tridceq  14365