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  3435  elexOLD  3466  rmoan  3707  rmoimi2  3711  reuan  3856  sstr2  3950  rabss2  4037  n0rex  4316  undif4  4426  r19.2zb  4455  rzal  4468  difprsnss  4759  snsspw  4804  uniin  4891  iuniin  4964  iuneq1  4968  iuneq2  4971  iunpwss  5066  axrep6  5238  axrep6OLD  5239  eunex  5340  rmorabex  5415  exss  5418  soeq2  5561  reliin  5771  coeq1  5811  coeq2  5812  cnveq  5827  dmeq  5857  dmin  5865  dmcoss  5927  rncoeq  5932  dminss  6114  imainss  6115  dfco2a  6207  iotaexOLD  6479  fundif  6549  fununi  6575  fof  6754  f1ocnv  6794  foco2  7063  isocnv  7287  isotr  7293  oprabidw  7400  oprabid  7401  zfrep6  7913  ovmptss  8049  dmtpos  8194  tposfn  8211  smores  8298  omopthlem1  8600  brinxper  8677  eqer  8684  fsetsspwxp  8803  ixpeq2  8861  enssdom  8925  fiprc  8993  sbthlem9  9036  infensuc  9096  fipwuni  9353  dfom3  9576  ttrcltr  9645  r1elss  9735  scott0  9815  fin56  10322  dominf  10374  ac6n  10414  brdom4  10459  dominfac  10502  inawina  10619  eltsk2g  10680  ltsosr  11023  ssxr  11219  recgt0ii  12065  sup2  12115  dfnn2  12175  peano2uz2  12598  eluzp1p1  12797  peano2uz  12836  ubmelfzo  13667  elfzlmr  13718  expclzlem  14024  wrdeq  14477  wwlktovf  14898  fsum2dlem  15712  fprod2dlem  15922  sin02gt0  16136  divalglem6  16344  qredeu  16604  isfunc  17806  xpcbas  18119  drsdirfi  18246  clatl  18449  tsrss  18530  mhmismgmhm  18700  smndex1mgm  18816  gimcnv  19181  gsum2dlem1  19884  gsum2dlem2  19885  rhmisrnghm  20400  subrngrng  20470  srhmsubclem1  20597  fldidom  20691  lmimcnv  21006  xrge0subm  21385  fctop  22924  cctop  22926  alexsubALTlem4  23970  lpbl  24424  xrge0gsumle  24755  xrge0tsms  24756  iirev  24856  iihalf1  24858  iihalf2  24861  iimulcl  24866  vitalilem1  25542  ply1idom  26063  aacjcl  26268  aannenlem2  26270  ang180lem4  26755  lgslem3  27243  sltval2  27601  madef  27801  lrrecfr  27890  norecdiv  28133  elons2  28199  dfn0s2  28264  nnaddscl  28278  nnmulscl  28279  znegscl  28320  uzsind  28333  zsoring  28336  zs12negscl  28390  renegscl  28402  readdscl  28403  remulscl  28406  tgjustf  28453  axlowdim  28941  axcontlem2  28945  usgrexmplef  29239  cusgrop  29418  rusgrpropedg  29565  spthispth  29704  pthdifv  29710  cycliscrct  29779  wwlksn0  29843  clwwlkccat  29969  clwwlkn  30005  clwwlknonccat  30075  numclwwlk1  30340  nmobndseqi  30758  axhcompl-zf  30977  hhcmpl  31179  shunssi  31347  spansni  31536  pjoml3i  31565  cmcmlem  31570  nonbooli  31630  lnopco0i  31983  pjnmopi  32127  pjnormssi  32147  hatomistici  32341  cvexchi  32348  cmdmdi  32396  mddmdin0i  32410  cdj3lem3b  32419  rmoun  32473  disjin  32565  disjin2  32566  xrge0tsmsd  33045  issgon  34106  sxbrsigalem0  34255  eulerpartlemgs2  34364  ballotlem2  34473  ballotth  34522  bnj945  34756  bnj556  34883  bnj557  34884  bnj607  34899  bnj864  34905  bnj969  34929  bnj999  34941  bnj1398  35017  wevgblacfn  35089  elpotr  35762  dfon2lem8  35771  txpss3v  35859  meran1  36392  arg-ax  36397  bj-nfalt  36692  bj-imdirco  37171  difunieq  37355  pibt1  37397  wl-cbvmotv  37494  poimirlem25  37632  poimirlem30  37637  bndss  37773  fldcrngo  37991  flddmn  38045  xrnss3v  38347  trressn  38429  redundss3  38612  redundpim3  38614  eldisjim  38769  eldisjim2  38770  eldisjn0el  38791  partim  38793  mainer  38819  prter1  38865  sn-sup2  42472  rimcnv  42498  fimgmcyclem  42514  mzpclall  42708  setindtrs  43007  dgraalem  43127  oneptri  43239  ifpimim  43491  inintabss  43560  refimssco  43589  cotrintab  43596  intimass  43636  psshepw  43770  nzin  44300  axc11next  44388  iotaexeu  44400  hbexgVD  44888  orbitclmpt  44941  wfaxrep  44977  wfaxsep  44978  wfaxpow  44980  wfaxpr  44981  wfac8prim  44985  permaxinf2lem  44995  absnsb  47021  aovpcov0  47184  aov0ov0  47187  ichan  47449  ichal  47460  spr0el  47476  sprsymrelf  47489  enege  47639  onego  47640  gbogbow  47750  gpgvtxedg0  48047  gpgvtxedg1  48048  gpgprismgr4cycllem10  48087  sgrpplusgaopALT  48176  rhmsubcALTVlem3  48264  eluz2cnn0n1  48493  regt1loggt0  48518  rege1logbrege0  48540  rege1logbzge0  48541  relogbmulbexp  48543  islan2  49608