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  2812  rmoan  3004  rmoimi2  3007  sseq2  3249  rabss2  3308  unssdif  3440  inssdif  3441  unssin  3444  inssun  3445  rabn0r  3519  undif4  3555  ssdif0im  3557  inssdif0im  3560  ssundifim  3576  ralf0  3595  prmg  3792  difprsnss  3809  snsspw  3845  pwprss  3887  pwtpss  3888  uniin  3911  intss  3947  iuniin  3978  iuneq1  3981  iuneq2  3984  iundif2ss  4034  iinuniss  4051  iunpwss  4060  intexrabim  4241  exmidundif  4294  exmidundifim  4295  exss  4317  pwunss  4378  soeq2  4411  ordunisuc2r  4610  peano5  4694  reliin  4847  coeq1  4885  coeq2  4886  cnveq  4902  dmeq  4929  dmin  4937  dmcoss  5000  rncoeq  5004  resiexg  5056  dminss  5149  imainss  5150  dfco2a  5235  euiotaex  5301  eliotaeu  5313  fundif  5371  fununi  5395  fof  5556  f1ocnv  5593  rexrnmpt  5786  isocnv  5947  isotr  5952  oprabid  6045  dmtpos  6417  tposfn  6434  smores  6453  eqer  6729  ixpeq2  6876  enssdom  6930  fiprc  6985  fiintim  7116  ltexprlemlol  7812  ltexprlemupu  7814  recexgt0  8750  peano2uz2  9577  eluzp1p1  9772  peano2uz  9807  zq  9850  ubmelfzo  10435  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  expclzaplem  10815  hashfiv01gt1  11034  wrdeq  11125  fsum2dlemstep  11985  fprod2dlemstep  12173  sin02gt0  12315  qredeu  12659  prmdc  12692  subrngrng  14206  lgslem3  15721  clwwlkccat  16196  clwwlknonccat  16228  bj-stim  16278  bj-stan  16279  bj-stal  16281  bj-nfalt  16296  bj-indint  16462  tridceq  16596