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  1826  excomimw  2045  nexmo  2539  eu6im  2573  ralimi2  3066  reximi2  3067  rabid2im  3429  elexOLD  3460  rmoan  3695  rmoimi2  3699  reuan  3844  sstr2  3938  rabss2OLD  4028  n0rex  4307  undif4  4417  rzal  4445  difprsnss  4753  snsspw  4798  uniin  4885  iuniin  4957  iuneq1  4961  iuneq2  4964  iunpwss  5060  axrep6  5231  axrep6OLD  5232  eunex  5333  rmorabex  5406  exss  5409  soeq2  5552  reliin  5764  coeq1  5804  coeq2  5805  cnveq  5820  dmeq  5850  dmin  5858  dmcoss  5922  dmcossOLD  5923  rncoeq  5929  dminss  6109  imainss  6110  dfco2a  6202  fundif  6539  fununi  6565  fof  6744  f1ocnv  6784  foco2  7052  isocnv  7274  isotr  7280  oprabidw  7387  oprabid  7388  zfrep6  7897  ovmptss  8033  dmtpos  8178  tposfn  8195  smores  8282  omopthlem1  8585  brinxper  8662  eqer  8669  fsetsspwxp  8788  ixpeq2  8847  enssdomOLD  8912  fiprc  8979  sbthlem9  9021  infensuc  9081  fipwuni  9327  dfom3  9554  ttrcltr  9623  r1elss  9716  scott0  9796  fin56  10301  dominf  10353  ac6n  10393  brdom4  10438  dominfac  10482  inawina  10599  eltsk2g  10660  ltsosr  11003  ssxr  11200  recgt0ii  12046  sup2  12096  dfnn2  12156  peano2uz2  12578  eluzp1p1  12777  peano2uz  12812  ubmelfzo  13644  elfzlmr  13696  expclzlem  14004  wrdeq  14457  wwlktovf  14877  fsum2dlem  15691  fprod2dlem  15901  sin02gt0  16115  divalglem6  16323  qredeu  16583  isfunc  17786  xpcbas  18099  drsdirfi  18226  clatl  18429  tsrss  18510  mhmismgmhm  18714  smndex1mgm  18830  gimcnv  19194  gsum2dlem1  19897  gsum2dlem2  19898  rhmisrnghm  20414  subrngrng  20481  srhmsubclem1  20608  fldidom  20702  lmimcnv  21017  xrge0subm  21396  fctop  22946  cctop  22948  alexsubALTlem4  23992  lpbl  24445  xrge0gsumle  24776  xrge0tsms  24777  iirev  24877  iihalf1  24879  iihalf2  24882  iimulcl  24887  vitalilem1  25563  ply1idom  26084  aacjcl  26289  aannenlem2  26291  ang180lem4  26776  lgslem3  27264  sltval2  27622  madef  27824  lrrecfr  27913  norecdiv  28159  elons2  28226  dfn0s2  28292  nnaddscl  28306  nnmulscl  28307  znegscl  28350  uzsind  28363  zsoring  28367  zs12negscl  28427  renegscl  28443  readdscl  28444  remulscl  28447  tgjustf  28494  axlowdim  28983  axcontlem2  28987  usgrexmplef  29281  cusgrop  29460  rusgrpropedg  29607  spthispth  29746  pthdifv  29752  cycliscrct  29821  wwlksn0  29885  clwwlkccat  30014  clwwlkn  30050  clwwlknonccat  30120  numclwwlk1  30385  nmobndseqi  30803  axhcompl-zf  31022  hhcmpl  31224  shunssi  31392  spansni  31581  pjoml3i  31610  cmcmlem  31615  nonbooli  31675  lnopco0i  32028  pjnmopi  32172  pjnormssi  32192  hatomistici  32386  cvexchi  32393  cmdmdi  32441  mddmdin0i  32455  cdj3lem3b  32464  rmoun  32517  disjin  32610  disjin2  32611  xrge0tsmsd  33104  issgon  34229  sxbrsigalem0  34377  eulerpartlemgs2  34486  ballotlem2  34595  ballotth  34644  bnj945  34878  bnj556  35005  bnj557  35006  bnj607  35021  bnj864  35027  bnj969  35051  bnj999  35063  bnj1398  35139  wevgblacfn  35252  elpotr  35922  dfon2lem8  35931  txpss3v  36019  meran1  36554  arg-ax  36559  bj-nfalt  36855  bj-imdirco  37334  difunieq  37518  pibt1  37560  wl-cbvmotv  37657  poimirlem25  37785  poimirlem30  37790  bndss  37926  fldcrngo  38144  flddmn  38198  xrnss3v  38505  trressn  38647  redundss3  38824  redundpim3  38826  eldisjim  38982  eldisjim2  38983  eldisjn0el  39004  partim  39006  mainer  39032  prter1  39078  sn-sup2  42688  rimcnv  42714  fimgmcyclem  42730  mzpclall  42911  setindtrs  43209  dgraalem  43329  oneptri  43441  ifpimim  43692  inintabss  43761  refimssco  43790  cotrintab  43797  intimass  43837  psshepw  43971  nzin  44501  axc11next  44589  iotaexeu  44601  hbexgVD  45088  orbitclmpt  45141  wfaxrep  45177  wfaxsep  45178  wfaxpow  45180  wfaxpr  45181  wfac8prim  45185  permaxinf2lem  45195  absnsb  47215  aovpcov0  47378  aov0ov0  47381  ichan  47643  ichal  47654  spr0el  47670  sprsymrelf  47683  enege  47833  onego  47834  gbogbow  47944  gpgvtxedg0  48251  gpgvtxedg1  48252  gpgprismgr4cycllem10  48292  sgrpplusgaopALT  48383  rhmsubcALTVlem3  48471  eluz2cnn0n1  48699  regt1loggt0  48724  rege1logbrege0  48746  rege1logbzge0  48747  relogbmulbexp  48749  islan2  49813