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  3207  rabss2  3266  unssdif  3398  inssdif  3399  unssin  3402  inssun  3403  rabn0r  3477  undif4  3513  ssdif0im  3515  inssdif0im  3518  ssundifim  3534  ralf0  3553  prmg  3743  difprsnss  3760  snsspw  3794  pwprss  3835  pwtpss  3836  uniin  3859  intss  3895  iuniin  3926  iuneq1  3929  iuneq2  3932  iundif2ss  3982  iinuniss  3999  iunpwss  4008  intexrabim  4186  exmidundif  4239  exmidundifim  4240  exss  4260  pwunss  4318  soeq2  4351  ordunisuc2r  4550  peano5  4634  reliin  4785  coeq1  4823  coeq2  4824  cnveq  4840  dmeq  4866  dmin  4874  dmcoss  4935  rncoeq  4939  resiexg  4991  dminss  5084  imainss  5085  dfco2a  5170  euiotaex  5235  eliotaeu  5247  fununi  5326  fof  5480  f1ocnv  5517  rexrnmpt  5705  isocnv  5858  isotr  5863  oprabid  5954  dmtpos  6314  tposfn  6331  smores  6350  eqer  6624  ixpeq2  6771  enssdom  6821  fiprc  6874  fiintim  6992  ltexprlemlol  7669  ltexprlemupu  7671  recexgt0  8607  peano2uz2  9433  eluzp1p1  9627  peano2uz  9657  zq  9700  ubmelfzo  10276  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  expclzaplem  10655  hashfiv01gt1  10874  wrdeq  10957  fsum2dlemstep  11599  fprod2dlemstep  11787  sin02gt0  11929  qredeu  12265  prmdc  12298  subrngrng  13758  lgslem3  15243  bj-stim  15392  bj-stan  15393  bj-stal  15395  bj-nfalt  15410  bj-indint  15577  tridceq  15700