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  847  stdcn  852  ifpdc  985  xordc1  1435  hbxfrbi  1518  nfalt  1624  19.29r  1667  19.31r  1727  sbimi  1810  spsbbi  1890  sbi2v  1939  euan  2134  2exeu  2170  ralimi2  2590  reximi2  2626  r19.28av  2667  r19.29r  2669  elex  2811  rmoan  3003  rmoimi2  3006  sseq2  3248  rabss2  3307  unssdif  3439  inssdif  3440  unssin  3443  inssun  3444  rabn0r  3518  undif4  3554  ssdif0im  3556  inssdif0im  3559  ssundifim  3575  ralf0  3594  prmg  3788  difprsnss  3805  snsspw  3841  pwprss  3883  pwtpss  3884  uniin  3907  intss  3943  iuniin  3974  iuneq1  3977  iuneq2  3980  iundif2ss  4030  iinuniss  4047  iunpwss  4056  intexrabim  4236  exmidundif  4289  exmidundifim  4290  exss  4312  pwunss  4373  soeq2  4406  ordunisuc2r  4605  peano5  4689  reliin  4840  coeq1  4878  coeq2  4879  cnveq  4895  dmeq  4922  dmin  4930  dmcoss  4993  rncoeq  4997  resiexg  5049  dminss  5142  imainss  5143  dfco2a  5228  euiotaex  5294  eliotaeu  5306  fundif  5364  fununi  5388  fof  5547  f1ocnv  5584  rexrnmpt  5777  isocnv  5934  isotr  5939  oprabid  6032  dmtpos  6400  tposfn  6417  smores  6436  eqer  6710  ixpeq2  6857  enssdom  6911  fiprc  6966  fiintim  7089  ltexprlemlol  7785  ltexprlemupu  7787  recexgt0  8723  peano2uz2  9550  eluzp1p1  9744  peano2uz  9774  zq  9817  ubmelfzo  10401  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  expclzaplem  10780  hashfiv01gt1  10999  wrdeq  11088  fsum2dlemstep  11940  fprod2dlemstep  12128  sin02gt0  12270  qredeu  12614  prmdc  12647  subrngrng  14160  lgslem3  15675  bj-stim  16068  bj-stan  16069  bj-stal  16071  bj-nfalt  16086  bj-indint  16252  tridceq  16383