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  1827  excomimw  2046  nexmo  2542  eu6im  2576  ralimi2  3070  reximi2  3071  rabid2im  3433  elexOLD  3464  rmoan  3699  rmoimi2  3703  reuan  3848  sstr2  3942  rabss2OLD  4032  n0rex  4311  undif4  4421  rzal  4449  difprsnss  4757  snsspw  4802  uniin  4889  iuniin  4961  iuneq1  4965  iuneq2  4968  iunpwss  5064  axrep6  5235  axrep6OLD  5236  eunex  5337  rmorabex  5415  exss  5418  soeq2  5562  reliin  5774  coeq1  5814  coeq2  5815  cnveq  5830  dmeq  5860  dmin  5868  dmcoss  5932  dmcossOLD  5933  rncoeq  5939  dminss  6119  imainss  6120  dfco2a  6212  fundif  6549  fununi  6575  fof  6754  f1ocnv  6794  foco2  7063  isocnv  7286  isotr  7292  oprabidw  7399  oprabid  7400  zfrep6  7909  ovmptss  8045  dmtpos  8190  tposfn  8207  smores  8294  omopthlem1  8597  brinxper  8675  eqer  8682  fsetsspwxp  8802  ixpeq2  8861  enssdomOLD  8926  fiprc  8993  sbthlem9  9035  infensuc  9095  fipwuni  9341  dfom3  9568  ttrcltr  9637  r1elss  9730  scott0  9810  fin56  10315  dominf  10367  ac6n  10407  brdom4  10452  dominfac  10496  inawina  10613  eltsk2g  10674  ltsosr  11017  ssxr  11214  recgt0ii  12060  sup2  12110  dfnn2  12170  peano2uz2  12592  eluzp1p1  12791  peano2uz  12826  ubmelfzo  13658  elfzlmr  13710  expclzlem  14018  wrdeq  14471  wwlktovf  14891  fsum2dlem  15705  fprod2dlem  15915  sin02gt0  16129  divalglem6  16337  qredeu  16597  isfunc  17800  xpcbas  18113  drsdirfi  18240  clatl  18443  tsrss  18524  mhmismgmhm  18728  smndex1mgm  18844  gimcnv  19208  gsum2dlem1  19911  gsum2dlem2  19912  rhmisrnghm  20428  subrngrng  20495  srhmsubclem1  20622  fldidom  20716  lmimcnv  21031  xrge0subm  21410  fctop  22960  cctop  22962  alexsubALTlem4  24006  lpbl  24459  xrge0gsumle  24790  xrge0tsms  24791  iirev  24891  iihalf1  24893  iihalf2  24896  iimulcl  24901  vitalilem1  25577  ply1idom  26098  aacjcl  26303  aannenlem2  26305  ang180lem4  26790  lgslem3  27278  ltsval2  27636  madef  27844  lrrecfr  27951  norecdiv  28198  elons2  28266  dfn0s2  28340  nnaddscl  28354  nnmulscl  28355  znegscl  28400  uzsind  28413  zsoring  28417  z12negscl  28486  renegscl  28506  readdscl  28507  remulscl  28510  tgjustf  28557  axlowdim  29046  axcontlem2  29050  usgrexmplef  29344  cusgrop  29523  rusgrpropedg  29670  spthispth  29809  pthdifv  29815  cycliscrct  29884  wwlksn0  29948  clwwlkccat  30077  clwwlkn  30113  clwwlknonccat  30183  numclwwlk1  30448  nmobndseqi  30867  axhcompl-zf  31086  hhcmpl  31288  shunssi  31456  spansni  31645  pjoml3i  31674  cmcmlem  31679  nonbooli  31739  lnopco0i  32092  pjnmopi  32236  pjnormssi  32256  hatomistici  32450  cvexchi  32457  cmdmdi  32505  mddmdin0i  32519  cdj3lem3b  32528  rmoun  32580  disjin  32673  disjin2  32674  xrge0tsmsd  33167  issgon  34301  sxbrsigalem0  34449  eulerpartlemgs2  34558  ballotlem2  34667  ballotth  34716  bnj945  34950  bnj556  35076  bnj557  35077  bnj607  35092  bnj864  35098  bnj969  35122  bnj999  35134  bnj1398  35210  wevgblacfn  35325  elpotr  35995  dfon2lem8  36004  txpss3v  36092  meran1  36627  arg-ax  36632  bj-nfalt  36956  bj-imdirco  37445  difunieq  37629  pibt1  37671  wl-cbvmotv  37768  poimirlem25  37896  poimirlem30  37901  bndss  38037  fldcrngo  38255  flddmn  38309  xrnss3v  38632  trressn  38786  redundss3  38963  redundpim3  38965  eldisjim  39138  eldisjim2  39139  eldisjn0el  39160  partim  39162  mainer  39199  prter1  39255  sn-sup2  42861  rimcnv  42887  fimgmcyclem  42903  mzpclall  43084  setindtrs  43382  dgraalem  43502  oneptri  43614  ifpimim  43865  inintabss  43934  refimssco  43963  cotrintab  43970  intimass  44010  psshepw  44144  nzin  44674  axc11next  44762  iotaexeu  44774  hbexgVD  45261  orbitclmpt  45314  wfaxrep  45350  wfaxsep  45351  wfaxpow  45353  wfaxpr  45354  wfac8prim  45358  permaxinf2lem  45368  absnsb  47387  aovpcov0  47550  aov0ov0  47553  ichan  47815  ichal  47826  spr0el  47842  sprsymrelf  47855  enege  48005  onego  48006  gbogbow  48116  gpgvtxedg0  48423  gpgvtxedg1  48424  gpgprismgr4cycllem10  48464  sgrpplusgaopALT  48555  rhmsubcALTVlem3  48643  eluz2cnn0n1  48871  regt1loggt0  48896  rege1logbrege0  48918  rege1logbzge0  48919  relogbmulbexp  48921  islan2  49985