Theorem 3imtr4i 200

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 120	. 2 ⊢ (𝜒 → 𝜓)
4		3imtr4.3	. 2 ⊢ (𝜃 ↔ 𝜓)
5	3, 4	sylibr 133	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  dcn  828  stdcn  833  dcan  919  xordc1  1372  hbxfrbi  1449  nfalt  1558  19.29r  1601  19.31r  1660  sbimi  1738  spsbbi  1817  sbi2v  1865  euan  2056  2exeu  2092  ralimi2  2495  reximi2  2531  r19.28av  2571  r19.29r  2573  elex  2700  rmoan  2888  rmoimi2  2891  sseq2  3126  rabss2  3185  unssdif  3316  inssdif  3317  unssin  3320  inssun  3321  rabn0r  3394  undif4  3430  ssdif0im  3432  inssdif0im  3435  ssundifim  3451  ralf0  3471  prmg  3652  difprsnss  3666  snsspw  3699  pwprss  3740  pwtpss  3741  uniin  3764  intss  3800  iuniin  3831  iuneq1  3834  iuneq2  3837  iundif2ss  3886  iinuniss  3903  iunpwss  3912  intexrabim  4086  exmidundif  4137  exmidundifim  4138  exss  4157  pwunss  4213  soeq2  4246  ordunisuc2r  4438  peano5  4520  reliin  4669  coeq1  4704  coeq2  4705  cnveq  4721  dmeq  4747  dmin  4755  dmcoss  4816  rncoeq  4820  resiexg  4872  dminss  4961  imainss  4962  dfco2a  5047  euiotaex  5112  fununi  5199  fof  5353  f1ocnv  5388  rexrnmpt  5571  isocnv  5720  isotr  5725  oprabid  5811  dmtpos  6161  tposfn  6178  smores  6197  eqer  6469  ixpeq2  6614  enssdom  6664  fiprc  6717  fiintim  6825  ltexprlemlol  7434  ltexprlemupu  7436  recexgt0  8366  peano2uz2  9182  eluzp1p1  9375  peano2uz  9405  zq  9445  ubmelfzo  10008  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  expclzaplem  10348  hashfiv01gt1  10560  fsum2dlemstep  11235  sin02gt0  11506  qredeu  11814  bj-stim  13125  bj-stan  13126  bj-stal  13128  bj-nfalt  13142  bj-indint  13300