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  1822  excomimw  2041  nexmo  2539  moimi  2543  eu6im  2573  ralimi2  3076  reximi2  3077  rexbiOLD  3103  rabid2im  3467  elexOLD  3500  rmoan  3748  rmoimi2  3752  reuan  3905  sstr2  4002  sseq2  4022  rabss2  4088  n0rex  4363  undif4  4473  r19.2zb  4502  rzal  4515  difprsnss  4804  snsspw  4849  uniin  4936  iuniin  5009  iuneq1  5013  iuneq2  5016  iunpwss  5112  axrep6  5294  axrep6OLD  5295  eunex  5396  rmorabex  5471  exss  5474  soeq2  5619  elopaelxpOLD  5779  reliin  5830  coeq1  5871  coeq2  5872  cnveq  5887  dmeq  5917  dmin  5925  dmcoss  5988  rncoeq  5993  dminss  6175  imainss  6176  dfco2a  6268  iotaexOLD  6543  fundif  6617  fununi  6643  fof  6821  f1ocnv  6861  foco2  7129  isocnv  7350  isotr  7356  oprabidw  7462  oprabid  7463  zfrep6  7978  ovmptss  8117  dmtpos  8262  tposfn  8279  smores  8391  omopthlem1  8696  brinxper  8773  eqer  8780  fsetsspwxp  8892  ixpeq2  8950  enssdom  9016  fiprc  9084  sbthlem9  9130  infensuc  9194  fipwuni  9464  dfom3  9685  ttrcltr  9754  r1elss  9844  scott0  9924  fin56  10431  dominf  10483  ac6n  10523  brdom4  10568  dominfac  10611  inawina  10728  eltsk2g  10789  ltsosr  11132  ssxr  11328  recgt0ii  12172  sup2  12222  dfnn2  12277  peano2uz2  12704  eluzp1p1  12904  peano2uz  12941  ubmelfzo  13766  elfzlmr  13817  expclzlem  14121  wrdeq  14571  wwlktovf  14992  fsum2dlem  15803  fprod2dlem  16013  sin02gt0  16225  divalglem6  16432  qredeu  16692  isfunc  17915  xpcbas  18234  drsdirfi  18363  clatl  18566  tsrss  18647  mhmismgmhm  18817  smndex1mgm  18933  gimcnv  19298  gsum2dlem1  20003  gsum2dlem2  20004  rhmisrnghm  20497  subrngrng  20567  srhmsubclem1  20694  fldidom  20788  lmimcnv  21084  xrge0subm  21443  fctop  23027  cctop  23029  alexsubALTlem4  24074  lpbl  24532  xrge0gsumle  24869  xrge0tsms  24870  iirev  24970  iihalf1  24972  iihalf2  24975  iimulcl  24980  vitalilem1  25657  ply1idom  26179  aacjcl  26384  aannenlem2  26386  ang180lem4  26870  lgslem3  27358  sltval2  27716  madef  27910  lrrecfr  27991  norecdiv  28231  elons2  28296  dfn0s2  28351  nnaddscl  28364  nnmulscl  28365  znegscl  28393  uzsind  28406  renegscl  28445  readdscl  28446  remulscl  28449  tgjustf  28496  axlowdim  28991  axcontlem2  28995  usgrexmplef  29291  cusgrop  29470  rusgrpropedg  29617  spthispth  29759  cycliscrct  29832  wwlksn0  29893  clwwlkccat  30019  clwwlkn  30055  clwwlknonccat  30125  numclwwlk1  30390  nmobndseqi  30808  axhcompl-zf  31027  hhcmpl  31229  shunssi  31397  spansni  31586  pjoml3i  31615  cmcmlem  31620  nonbooli  31680  lnopco0i  32033  pjnmopi  32177  pjnormssi  32197  hatomistici  32391  cvexchi  32398  cmdmdi  32446  mddmdin0i  32460  cdj3lem3b  32469  rmoun  32522  disjin  32606  disjin2  32607  xrge0tsmsd  33048  issgon  34104  sxbrsigalem0  34253  eulerpartlemgs2  34362  ballotlem2  34470  ballotth  34519  bnj945  34766  bnj556  34893  bnj557  34894  bnj607  34909  bnj864  34915  bnj969  34939  bnj999  34951  bnj1398  35027  wevgblacfn  35093  elpotr  35763  dfon2lem8  35772  txpss3v  35860  meran1  36394  arg-ax  36399  bj-nfalt  36694  bj-imdirco  37173  difunieq  37357  pibt1  37399  wl-cbvmotv  37494  poimirlem25  37632  poimirlem30  37637  bndss  37773  fldcrngo  37991  flddmn  38045  xrnss3v  38354  trressn  38427  redundss3  38610  redundpim3  38612  eldisjim  38766  eldisjim2  38767  eldisjn0el  38788  partim  38790  mainer  38816  prter1  38861  sn-sup2  42478  rimcnv  42504  fimgmcyclem  42520  mzpclall  42715  setindtrs  43014  dgraalem  43134  oneptri  43246  ifpimim  43499  inintabss  43568  refimssco  43597  cotrintab  43604  intimass  43644  psshepw  43778  nzin  44314  axc11next  44402  iotaexeu  44414  hbexgVD  44904  wfaxrep  44950  wfaxsep  44951  wfaxpr  44952  absnsb  46977  aovpcov0  47140  aov0ov0  47143  ichan  47380  ichal  47391  spr0el  47407  sprsymrelf  47420  enege  47570  onego  47571  gbogbow  47681  gpgvtxedg0  47956  gpgvtxedg1  47957  sgrpplusgaopALT  48039  rhmsubcALTVlem3  48127  eluz2cnn0n1  48357  regt1loggt0  48386  rege1logbrege0  48408  rege1logbzge0  48409  relogbmulbexp  48411