Theorem 3imtr4i 292

Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-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 217	. 2 ⊢ (𝜒 → 𝜓)
4		3imtr4.3	. 2 ⊢ (𝜃 ↔ 𝜓)
5	3, 4	sylibr 234	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  hbxfrbi  1825  excomimw  2044  nexmo  2534  moimi  2538  eu6im  2568  ralimi2  3061  reximi2  3062  rabid2im  3427  elexOLD  3458  rmoan  3699  rmoimi2  3703  reuan  3848  sstr2  3942  rabss2  4029  n0rex  4308  undif4  4418  r19.2zb  4447  rzal  4460  difprsnss  4750  snsspw  4795  uniin  4882  iuniin  4954  iuneq1  4958  iuneq2  4961  iunpwss  5056  axrep6  5227  axrep6OLD  5228  eunex  5329  rmorabex  5403  exss  5406  soeq2  5549  reliin  5760  coeq1  5800  coeq2  5801  cnveq  5816  dmeq  5846  dmin  5854  dmcoss  5916  dmcossOLD  5917  rncoeq  5923  dminss  6102  imainss  6103  dfco2a  6195  fundif  6531  fununi  6557  fof  6736  f1ocnv  6776  foco2  7043  isocnv  7267  isotr  7273  oprabidw  7380  oprabid  7381  zfrep6  7890  ovmptss  8026  dmtpos  8171  tposfn  8188  smores  8275  omopthlem1  8577  brinxper  8654  eqer  8661  fsetsspwxp  8780  ixpeq2  8838  enssdom  8902  fiprc  8970  sbthlem9  9012  infensuc  9072  fipwuni  9316  dfom3  9543  ttrcltr  9612  r1elss  9702  scott0  9782  fin56  10287  dominf  10339  ac6n  10379  brdom4  10424  dominfac  10467  inawina  10584  eltsk2g  10645  ltsosr  10988  ssxr  11185  recgt0ii  12031  sup2  12081  dfnn2  12141  peano2uz2  12564  eluzp1p1  12763  peano2uz  12802  ubmelfzo  13633  elfzlmr  13684  expclzlem  13990  wrdeq  14443  wwlktovf  14863  fsum2dlem  15677  fprod2dlem  15887  sin02gt0  16101  divalglem6  16309  qredeu  16569  isfunc  17771  xpcbas  18084  drsdirfi  18211  clatl  18414  tsrss  18495  mhmismgmhm  18665  smndex1mgm  18781  gimcnv  19146  gsum2dlem1  19849  gsum2dlem2  19850  rhmisrnghm  20365  subrngrng  20435  srhmsubclem1  20562  fldidom  20656  lmimcnv  20971  xrge0subm  21350  fctop  22889  cctop  22891  alexsubALTlem4  23935  lpbl  24389  xrge0gsumle  24720  xrge0tsms  24721  iirev  24821  iihalf1  24823  iihalf2  24826  iimulcl  24831  vitalilem1  25507  ply1idom  26028  aacjcl  26233  aannenlem2  26235  ang180lem4  26720  lgslem3  27208  sltval2  27566  madef  27766  lrrecfr  27855  norecdiv  28098  elons2  28164  dfn0s2  28229  nnaddscl  28243  nnmulscl  28244  znegscl  28285  uzsind  28298  zsoring  28301  zs12negscl  28355  renegscl  28367  readdscl  28368  remulscl  28371  tgjustf  28418  axlowdim  28906  axcontlem2  28910  usgrexmplef  29204  cusgrop  29383  rusgrpropedg  29530  spthispth  29669  pthdifv  29675  cycliscrct  29744  wwlksn0  29808  clwwlkccat  29934  clwwlkn  29970  clwwlknonccat  30040  numclwwlk1  30305  nmobndseqi  30723  axhcompl-zf  30942  hhcmpl  31144  shunssi  31312  spansni  31501  pjoml3i  31530  cmcmlem  31535  nonbooli  31595  lnopco0i  31948  pjnmopi  32092  pjnormssi  32112  hatomistici  32306  cvexchi  32313  cmdmdi  32361  mddmdin0i  32375  cdj3lem3b  32384  rmoun  32438  disjin  32530  disjin2  32531  xrge0tsmsd  33016  issgon  34096  sxbrsigalem0  34245  eulerpartlemgs2  34354  ballotlem2  34463  ballotth  34512  bnj945  34746  bnj556  34873  bnj557  34874  bnj607  34889  bnj864  34895  bnj969  34919  bnj999  34931  bnj1398  35007  wevgblacfn  35092  elpotr  35765  dfon2lem8  35774  txpss3v  35862  meran1  36395  arg-ax  36400  bj-nfalt  36695  bj-imdirco  37174  difunieq  37358  pibt1  37400  wl-cbvmotv  37497  poimirlem25  37635  poimirlem30  37640  bndss  37776  fldcrngo  37994  flddmn  38048  xrnss3v  38350  trressn  38432  redundss3  38615  redundpim3  38617  eldisjim  38772  eldisjim2  38773  eldisjn0el  38794  partim  38796  mainer  38822  prter1  38868  sn-sup2  42474  rimcnv  42500  fimgmcyclem  42516  mzpclall  42710  setindtrs  43008  dgraalem  43128  oneptri  43240  ifpimim  43492  inintabss  43561  refimssco  43590  cotrintab  43597  intimass  43637  psshepw  43771  nzin  44301  axc11next  44389  iotaexeu  44401  hbexgVD  44889  orbitclmpt  44942  wfaxrep  44978  wfaxsep  44979  wfaxpow  44981  wfaxpr  44982  wfac8prim  44986  permaxinf2lem  44996  absnsb  47021  aovpcov0  47184  aov0ov0  47187  ichan  47449  ichal  47460  spr0el  47476  sprsymrelf  47489  enege  47639  onego  47640  gbogbow  47750  gpgvtxedg0  48057  gpgvtxedg1  48058  gpgprismgr4cycllem10  48098  sgrpplusgaopALT  48189  rhmsubcALTVlem3  48277  eluz2cnn0n1  48506  regt1loggt0  48531  rege1logbrege0  48553  rege1logbzge0  48554  relogbmulbexp  48556  islan2  49621