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  843  stdcn  848  xordc1  1404  hbxfrbi  1486  nfalt  1592  19.29r  1635  19.31r  1695  sbimi  1778  spsbbi  1858  sbi2v  1907  euan  2101  2exeu  2137  ralimi2  2557  reximi2  2593  r19.28av  2633  r19.29r  2635  elex  2774  rmoan  2964  rmoimi2  2967  sseq2  3208  rabss2  3267  unssdif  3399  inssdif  3400  unssin  3403  inssun  3404  rabn0r  3478  undif4  3514  ssdif0im  3516  inssdif0im  3519  ssundifim  3535  ralf0  3554  prmg  3744  difprsnss  3761  snsspw  3795  pwprss  3836  pwtpss  3837  uniin  3860  intss  3896  iuniin  3927  iuneq1  3930  iuneq2  3933  iundif2ss  3983  iinuniss  4000  iunpwss  4009  intexrabim  4187  exmidundif  4240  exmidundifim  4241  exss  4261  pwunss  4319  soeq2  4352  ordunisuc2r  4551  peano5  4635  reliin  4786  coeq1  4824  coeq2  4825  cnveq  4841  dmeq  4867  dmin  4875  dmcoss  4936  rncoeq  4940  resiexg  4992  dminss  5085  imainss  5086  dfco2a  5171  euiotaex  5236  eliotaeu  5248  fununi  5327  fof  5483  f1ocnv  5520  rexrnmpt  5708  isocnv  5861  isotr  5866  oprabid  5957  dmtpos  6323  tposfn  6340  smores  6359  eqer  6633  ixpeq2  6780  enssdom  6830  fiprc  6883  fiintim  7001  ltexprlemlol  7688  ltexprlemupu  7690  recexgt0  8626  peano2uz2  9452  eluzp1p1  9646  peano2uz  9676  zq  9719  ubmelfzo  10295  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  expclzaplem  10674  hashfiv01gt1  10893  wrdeq  10976  fsum2dlemstep  11618  fprod2dlemstep  11806  sin02gt0  11948  qredeu  12292  prmdc  12325  subrngrng  13836  lgslem3  15351  bj-stim  15500  bj-stan  15501  bj-stal  15503  bj-nfalt  15518  bj-indint  15685  tridceq  15813