Theorem 3imtr4i 295

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 220	. 2 ⊢ (𝜒 → 𝜓)
4		3imtr4.3	. 2 ⊢ (𝜃 ↔ 𝜓)
5	3, 4	sylibr 237	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  hbxfrbi  1852  excomimw  2071  nexmo  2575  eu6im  2609  ralimi2  3103  reximi2  3104  rabid2im  3455  rmoan  3711  rmoimi2  3715  reuan  3858  sstr2  3952  rabss2OLD  4040  n0rex  4320  undif4  4433  rzal  4460  difprsnss  4771  snsspw  4813  uniinOLD  4901  iuniin  4973  iuneq1  4977  iuneq2  4980  iunpwss  5077  axrep6  5251  axrep6OLD  5252  eunex  5362  rmorabex  5442  exss  5445  soeq2  5592  reliin  5805  coeq1  5844  coeq2  5845  cnveq  5860  dmeq  5894  dmin  5902  dmcoss  5966  dmcossOLD  5967  rncoeq  5972  dminss  6151  imainss  6152  dfco2a  6248  fundif  6586  fununi  6612  fof  6793  f1ocnv  6834  foco2  7105  isocnv  7329  isotr  7335  oprabidw  7442  oprabid  7443  zfrep6OLD  7952  ovmptss  8088  dmtpos  8234  tposfn  8251  smores  8339  omopthlem1  8645  brinxper  8724  eqer  8731  fsetsspwxp  8850  ixpeq2  8909  enssdomOLD  8974  fiprc  9041  sbthlem9  9083  infensuc  9143  fipwuni  9386  dfom3  9616  ttrcltr  9685  r1elss  9778  scott0  9860  fin56  10377  dominf  10429  ac6n  10469  brdom4  10514  dominfac  10558  inawina  10675  eltsk2g  10736  ltsosr  11079  ssxr  11279  recgt0ii  12121  sup2  12171  dfnn2  12246  peano2uz2  12684  eluzp1p1  12890  peano2uz  12925  ubmelfzo  13759  elfzlmr  13811  expclzlem  14119  wrdeq  14573  wwlktovf  14993  fsum2dlem  15821  fprod2dlem  16034  sin02gt0  16248  divalglem6  16456  qredeu  16716  isfunc  17921  xpcbas  18234  drsdirfi  18361  clatl  18564  tsrss  18645  mhmismgmhm  18849  smndex1mgm  18969  gimcnv  19337  gsum2dlem1  20040  gsum2dlem2  20041  rhmisrnghm  20562  rimcnv  20567  subrngrng  20635  srhmsubclem1  20762  fldidom  20853  lmimcnv  21166  xrge0subm  21562  fctop  23130  cctop  23132  alexsubALTlem4  24176  lpbl  24629  xrge0gsumle  24960  xrge0tsms  24961  iirev  25057  iihalf1  25059  iihalf2  25061  iimulcl  25065  vitalilem1  25736  ply1idom  26251  aacjcl  26457  aannenlem2  26459  ang180lem4  26943  lgslem3  27429  ltsval2  27786  madef  27995  lrrecfr  28102  norecdiv  28349  elons2  28417  dfn0s2  28491  nnaddscl  28505  nnmulscl  28506  znegscl  28551  uzsind  28564  zsoring  28568  z12negscl  28637  renegscl  28657  readdscl  28658  remulscl  28661  tgjustf  28708  axlowdim  29252  axcontlem2  29256  usgrexmplef  29550  cusgrop  29729  rusgrpropedg  29875  spthispth  30014  pthdifv  30020  cycliscrct  30089  wwlksn0  30153  clwwlkccat  30282  clwwlkn  30318  clwwlknonccat  30388  numclwwlk1  30653  nmobndseqi  31072  axhcompl-zf  31291  hhcmpl  31493  shunssi  31661  spansni  31850  pjoml3i  31879  cmcmlem  31884  nonbooli  31944  lnopco0i  32297  pjnmopi  32441  pjnormssi  32461  hatomistici  32655  cvexchi  32662  cmdmdi  32710  mddmdin0i  32724  cdj3lem3b  32733  rmoun  32781  disjin  32872  disjin2  32873  xrge0tsmsd  33334  issgon  34458  sxbrsigalem0  34606  eulerpartlemgs2  34715  ballotlem2  34824  ballotth  34873  bnj945  35107  bnj556  35233  bnj557  35234  bnj607  35249  bnj864  35255  bnj969  35279  bnj999  35291  bnj1398  35367  wevgblacfn  35494  elpotr  36170  dfon2lem8  36179  txpss3v  36267  meran1  36811  arg-ax  36816  bj-sbcex  37162  bj-nfalt  37227  bj-imdirco  37722  difunieq  37908  pibt1  37950  wl-cbvmotv  38056  poimirlem25  38184  poimirlem30  38189  bndss  38325  fldcrngo  38543  flddmn  38597  xrnss3v  38920  trressn  39074  redundss3  39251  redundpim3  39253  eldisjim  39426  eldisjim2  39427  eldisjn0el  39448  partim  39450  mainer  39487  prter1  39543  sn-sup2  43155  fimgmcyclem  43193  mzpclall  43350  setindtrs  43644  dgraalem  43764  oneptri  43876  ifpimim  44127  inintabss  44196  refimssco  44225  cotrintab  44232  intimass  44272  psshepw  44406  nzin  44920  axc11next  45008  iotaexeu  45020  hbexgVD  45506  orbitclmpt  45559  wfaxrep  45595  wfaxsep  45596  wfaxpow  45598  wfaxpr  45599  wfac8prim  45603  permaxinf2lem  45613  absnsb  47653  aovpcov0  47816  aov0ov0  47819  muldvdsfacgt  48012  ichan  48093  ichal  48104  spr0el  48120  sprsymrelf  48133  enege  48299  onego  48300  gbogbow  48410  gpgvtxedg0  48717  gpgvtxedg1  48718  gpgprismgr4cycllem10  48758  sgrpplusgaopALT  48849  rhmsubcALTVlem3  48937  eluz2cnn0n1  49176  regt1loggt0  49201  rege1logbrege0  49223  rege1logbzge0  49224  relogbmulbexp  49226  islan2  50289