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  2536  moimi  2540  eu6im  2570  ralimi2  3064  reximi2  3065  rabid2im  3427  elexOLD  3458  rmoan  3693  rmoimi2  3697  reuan  3842  sstr2  3936  rabss2OLD  4025  n0rex  4304  undif4  4414  r19.2zb  4443  rzal  4456  difprsnss  4748  snsspw  4793  uniin  4880  iuniin  4952  iuneq1  4956  iuneq2  4959  iunpwss  5053  axrep6  5224  axrep6OLD  5225  eunex  5326  rmorabex  5398  exss  5401  soeq2  5544  reliin  5756  coeq1  5796  coeq2  5797  cnveq  5812  dmeq  5842  dmin  5850  dmcoss  5913  dmcossOLD  5914  rncoeq  5920  dminss  6100  imainss  6101  dfco2a  6193  fundif  6530  fununi  6556  fof  6735  f1ocnv  6775  foco2  7042  isocnv  7264  isotr  7270  oprabidw  7377  oprabid  7378  zfrep6  7887  ovmptss  8023  dmtpos  8168  tposfn  8185  smores  8272  omopthlem1  8574  brinxper  8651  eqer  8658  fsetsspwxp  8777  ixpeq2  8835  enssdom  8899  fiprc  8966  sbthlem9  9008  infensuc  9068  fipwuni  9310  dfom3  9537  ttrcltr  9606  r1elss  9699  scott0  9779  fin56  10284  dominf  10336  ac6n  10376  brdom4  10421  dominfac  10464  inawina  10581  eltsk2g  10642  ltsosr  10985  ssxr  11182  recgt0ii  12028  sup2  12078  dfnn2  12138  peano2uz2  12561  eluzp1p1  12760  peano2uz  12799  ubmelfzo  13630  elfzlmr  13682  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  18699  smndex1mgm  18815  gimcnv  19179  gsum2dlem1  19882  gsum2dlem2  19883  rhmisrnghm  20398  subrngrng  20465  srhmsubclem1  20592  fldidom  20686  lmimcnv  21001  xrge0subm  21380  fctop  22919  cctop  22921  alexsubALTlem4  23965  lpbl  24418  xrge0gsumle  24749  xrge0tsms  24750  iirev  24850  iihalf1  24852  iihalf2  24855  iimulcl  24860  vitalilem1  25536  ply1idom  26057  aacjcl  26262  aannenlem2  26264  ang180lem4  26749  lgslem3  27237  sltval2  27595  madef  27797  lrrecfr  27886  norecdiv  28129  elons2  28195  dfn0s2  28260  nnaddscl  28274  nnmulscl  28275  znegscl  28316  uzsind  28329  zsoring  28332  zs12negscl  28388  renegscl  28400  readdscl  28401  remulscl  28404  tgjustf  28451  axlowdim  28939  axcontlem2  28943  usgrexmplef  29237  cusgrop  29416  rusgrpropedg  29563  spthispth  29702  pthdifv  29708  cycliscrct  29777  wwlksn0  29841  clwwlkccat  29970  clwwlkn  30006  clwwlknonccat  30076  numclwwlk1  30341  nmobndseqi  30759  axhcompl-zf  30978  hhcmpl  31180  shunssi  31348  spansni  31537  pjoml3i  31566  cmcmlem  31571  nonbooli  31631  lnopco0i  31984  pjnmopi  32128  pjnormssi  32148  hatomistici  32342  cvexchi  32349  cmdmdi  32397  mddmdin0i  32411  cdj3lem3b  32420  rmoun  32473  disjin  32566  disjin2  32567  xrge0tsmsd  33042  issgon  34136  sxbrsigalem0  34284  eulerpartlemgs2  34393  ballotlem2  34502  ballotth  34551  bnj945  34785  bnj556  34912  bnj557  34913  bnj607  34928  bnj864  34934  bnj969  34958  bnj999  34970  bnj1398  35046  wevgblacfn  35153  elpotr  35823  dfon2lem8  35832  txpss3v  35920  meran1  36455  arg-ax  36460  bj-nfalt  36755  bj-imdirco  37234  difunieq  37418  pibt1  37460  wl-cbvmotv  37557  poimirlem25  37695  poimirlem30  37700  bndss  37836  fldcrngo  38054  flddmn  38108  xrnss3v  38415  trressn  38557  redundss3  38734  redundpim3  38736  eldisjim  38892  eldisjim2  38893  eldisjn0el  38914  partim  38916  mainer  38942  prter1  38988  sn-sup2  42594  rimcnv  42620  fimgmcyclem  42636  mzpclall  42830  setindtrs  43128  dgraalem  43248  oneptri  43360  ifpimim  43612  inintabss  43681  refimssco  43710  cotrintab  43717  intimass  43757  psshepw  43891  nzin  44421  axc11next  44509  iotaexeu  44521  hbexgVD  45008  orbitclmpt  45061  wfaxrep  45097  wfaxsep  45098  wfaxpow  45100  wfaxpr  45101  wfac8prim  45105  permaxinf2lem  45115  absnsb  47137  aovpcov0  47300  aov0ov0  47303  ichan  47565  ichal  47576  spr0el  47592  sprsymrelf  47605  enege  47755  onego  47756  gbogbow  47866  gpgvtxedg0  48173  gpgvtxedg1  48174  gpgprismgr4cycllem10  48214  sgrpplusgaopALT  48305  rhmsubcALTVlem3  48393  eluz2cnn0n1  48622  regt1loggt0  48647  rege1logbrege0  48669  rege1logbzge0  48670  relogbmulbexp  48672  islan2  49737