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  33015  issgon  34090  sxbrsigalem0  34239  eulerpartlemgs2  34348  ballotlem2  34457  ballotth  34506  bnj945  34740  bnj556  34867  bnj557  34868  bnj607  34883  bnj864  34889  bnj969  34913  bnj999  34925  bnj1398  35001  wevgblacfn  35086  elpotr  35759  dfon2lem8  35768  txpss3v  35856  meran1  36389  arg-ax  36394  bj-nfalt  36689  bj-imdirco  37168  difunieq  37352  pibt1  37394  wl-cbvmotv  37491  poimirlem25  37629  poimirlem30  37634  bndss  37770  fldcrngo  37988  flddmn  38042  xrnss3v  38344  trressn  38426  redundss3  38609  redundpim3  38611  eldisjim  38766  eldisjim2  38767  eldisjn0el  38788  partim  38790  mainer  38816  prter1  38862  sn-sup2  42468  rimcnv  42494  fimgmcyclem  42510  mzpclall  42704  setindtrs  43002  dgraalem  43122  oneptri  43234  ifpimim  43486  inintabss  43555  refimssco  43584  cotrintab  43591  intimass  43631  psshepw  43765  nzin  44295  axc11next  44383  iotaexeu  44395  hbexgVD  44883  orbitclmpt  44936  wfaxrep  44972  wfaxsep  44973  wfaxpow  44975  wfaxpr  44976  wfac8prim  44980  permaxinf2lem  44990  absnsb  47015  aovpcov0  47178  aov0ov0  47181  ichan  47443  ichal  47454  spr0el  47470  sprsymrelf  47483  enege  47633  onego  47634  gbogbow  47744  gpgvtxedg0  48051  gpgvtxedg1  48052  gpgprismgr4cycllem10  48092  sgrpplusgaopALT  48183  rhmsubcALTVlem3  48271  eluz2cnn0n1  48500  regt1loggt0  48525  rege1logbrege0  48547  rege1logbzge0  48548  relogbmulbexp  48550  islan2  49615