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  1483  nfalt  1589  19.29r  1632  19.31r  1692  sbimi  1775  spsbbi  1855  sbi2v  1904  euan  2094  2exeu  2130  ralimi2  2550  reximi2  2586  r19.28av  2626  r19.29r  2628  elex  2763  rmoan  2952  rmoimi2  2955  sseq2  3194  rabss2  3253  unssdif  3385  inssdif  3386  unssin  3389  inssun  3390  rabn0r  3464  undif4  3500  ssdif0im  3502  inssdif0im  3505  ssundifim  3521  ralf0  3541  prmg  3728  difprsnss  3745  snsspw  3779  pwprss  3820  pwtpss  3821  uniin  3844  intss  3880  iuniin  3911  iuneq1  3914  iuneq2  3917  iundif2ss  3967  iinuniss  3984  iunpwss  3993  intexrabim  4168  exmidundif  4221  exmidundifim  4222  exss  4242  pwunss  4298  soeq2  4331  ordunisuc2r  4528  peano5  4612  reliin  4763  coeq1  4799  coeq2  4800  cnveq  4816  dmeq  4842  dmin  4850  dmcoss  4911  rncoeq  4915  resiexg  4967  dminss  5058  imainss  5059  dfco2a  5144  euiotaex  5209  eliotaeu  5221  fununi  5300  fof  5454  f1ocnv  5490  rexrnmpt  5676  isocnv  5829  isotr  5834  oprabid  5924  dmtpos  6276  tposfn  6293  smores  6312  eqer  6586  ixpeq2  6733  enssdom  6783  fiprc  6836  fiintim  6952  ltexprlemlol  7626  ltexprlemupu  7628  recexgt0  8562  peano2uz2  9385  eluzp1p1  9578  peano2uz  9608  zq  9651  ubmelfzo  10225  frecuzrdgtcl  10438  frecuzrdgfunlem  10445  expclzaplem  10570  hashfiv01gt1  10789  fsum2dlemstep  11469  fprod2dlemstep  11657  sin02gt0  11798  qredeu  12124  prmdc  12157  subrngrng  13542  lgslem3  14841  bj-stim  14936  bj-stan  14937  bj-stal  14939  bj-nfalt  14954  bj-indint  15121  tridceq  15243