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 ⊢ (𝜒 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  dcn  854  stdcn  859  ifpdc  992  xordc1  1442  hbxfrbi  1525  nfalt  1631  19.29r  1674  19.31r  1733  sbimi  1817  spsbbi  1897  sbi2v  1947  euan  2143  2exeu  2179  ralimi2  2610  reximi2  2646  r19.28av  2687  r19.29r  2689  elex  2833  rmoan  3026  rmoimi2  3029  sseq2  3272  rabss2  3331  unssdif  3466  inssdif  3467  unssin  3470  inssun  3471  rabn0r  3548  undif4  3587  ssdif0im  3589  inssdif0imOLD  3593  ssundifim  3611  ralf0  3630  prmg  3835  difprsnss  3853  snsspw  3889  pwprss  3931  pwtpss  3932  uniin  3955  intss  3991  iuniin  4022  iuneq1  4025  iuneq2  4028  iundif2ss  4078  iinuniss  4095  iunpwss  4104  intexrabim  4289  exmidundif  4343  exmidundifim  4344  exss  4367  pwunss  4428  soeq2  4461  ordunisuc2r  4661  peano5  4745  reliin  4899  coeq1  4937  coeq2  4938  cnveq  4954  dmeq  4981  dmin  4989  dmcoss  5052  rncoeq  5056  resiexg  5108  dminss  5202  imainss  5203  dfco2a  5288  euiotaex  5354  eliotaeu  5366  fundif  5425  fununi  5449  fof  5615  f1ocnv  5652  rexrnmpt  5851  isocnv  6017  isotr  6022  oprabid  6117  dmtpos  6527  tposfn  6544  smores  6563  eqer  6839  fsetsspwxp  6948  ixpeq2  6994  enssdom  7048  fiprc  7104  fiintim  7238  ltexprlemlol  7969  ltexprlemupu  7971  recexgt0  8910  peano2uz2  9757  eluzp1p1  9957  peano2uz  9992  zq  10035  ubmelfzo  10628  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  expclzaplem  11013  hashfiv01gt1  11235  hashfibclem  11296  wrdeq  11340  fsum2dlemstep  12217  fprod2dlemstep  12405  sin02gt0  12547  qredeu  12891  prmdc  12924  ballotfilemth  13330  subrngrng  14559  lgslem3  16219  clwwlkccat  16740  clwwlknonccat  16772  bj-stim  16872  bj-stan  16873  bj-stal  16875  bj-nfalt  16890  bj-indint  17055  tridceq  17204  alseuals  17263  ralseurals  17264