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  3438  elexOLD  3469  rmoan  3710  rmoimi2  3714  reuan  3859  sstr2  3953  rabss2  4041  n0rex  4320  undif4  4430  r19.2zb  4459  rzal  4472  difprsnss  4763  snsspw  4808  uniin  4895  iuniin  4968  iuneq1  4972  iuneq2  4975  iunpwss  5071  axrep6  5243  axrep6OLD  5244  eunex  5345  rmorabex  5420  exss  5423  soeq2  5568  elopaelxpOLD  5729  reliin  5780  coeq1  5821  coeq2  5822  cnveq  5837  dmeq  5867  dmin  5875  dmcoss  5938  rncoeq  5943  dminss  6126  imainss  6127  dfco2a  6219  iotaexOLD  6491  fundif  6565  fununi  6591  fof  6772  f1ocnv  6812  foco2  7081  isocnv  7305  isotr  7311  oprabidw  7418  oprabid  7419  zfrep6  7933  ovmptss  8072  dmtpos  8217  tposfn  8234  smores  8321  omopthlem1  8623  brinxper  8700  eqer  8707  fsetsspwxp  8826  ixpeq2  8884  enssdom  8948  fiprc  9016  sbthlem9  9059  infensuc  9119  fipwuni  9377  dfom3  9600  ttrcltr  9669  r1elss  9759  scott0  9839  fin56  10346  dominf  10398  ac6n  10438  brdom4  10483  dominfac  10526  inawina  10643  eltsk2g  10704  ltsosr  11047  ssxr  11243  recgt0ii  12089  sup2  12139  dfnn2  12199  peano2uz2  12622  eluzp1p1  12821  peano2uz  12860  ubmelfzo  13691  elfzlmr  13742  expclzlem  14048  wrdeq  14501  wwlktovf  14922  fsum2dlem  15736  fprod2dlem  15946  sin02gt0  16160  divalglem6  16368  qredeu  16628  isfunc  17826  xpcbas  18139  drsdirfi  18266  clatl  18467  tsrss  18548  mhmismgmhm  18718  smndex1mgm  18834  gimcnv  19199  gsum2dlem1  19900  gsum2dlem2  19901  rhmisrnghm  20389  subrngrng  20459  srhmsubclem1  20586  fldidom  20680  lmimcnv  20974  xrge0subm  21324  fctop  22891  cctop  22893  alexsubALTlem4  23937  lpbl  24391  xrge0gsumle  24722  xrge0tsms  24723  iirev  24823  iihalf1  24825  iihalf2  24828  iimulcl  24833  vitalilem1  25509  ply1idom  26030  aacjcl  26235  aannenlem2  26237  ang180lem4  26722  lgslem3  27210  sltval2  27568  madef  27764  lrrecfr  27850  norecdiv  28093  elons2  28159  dfn0s2  28224  nnaddscl  28238  nnmulscl  28239  znegscl  28280  uzsind  28293  zs12negscl  28340  renegscl  28349  readdscl  28350  remulscl  28353  tgjustf  28400  axlowdim  28888  axcontlem2  28892  usgrexmplef  29186  cusgrop  29365  rusgrpropedg  29512  spthispth  29654  pthdifv  29660  cycliscrct  29729  wwlksn0  29793  clwwlkccat  29919  clwwlkn  29955  clwwlknonccat  30025  numclwwlk1  30290  nmobndseqi  30708  axhcompl-zf  30927  hhcmpl  31129  shunssi  31297  spansni  31486  pjoml3i  31515  cmcmlem  31520  nonbooli  31580  lnopco0i  31933  pjnmopi  32077  pjnormssi  32097  hatomistici  32291  cvexchi  32298  cmdmdi  32346  mddmdin0i  32360  cdj3lem3b  32369  rmoun  32423  disjin  32515  disjin2  32516  xrge0tsmsd  33002  issgon  34113  sxbrsigalem0  34262  eulerpartlemgs2  34371  ballotlem2  34480  ballotth  34529  bnj945  34763  bnj556  34890  bnj557  34891  bnj607  34906  bnj864  34912  bnj969  34936  bnj999  34948  bnj1398  35024  wevgblacfn  35096  elpotr  35769  dfon2lem8  35778  txpss3v  35866  meran1  36399  arg-ax  36404  bj-nfalt  36699  bj-imdirco  37178  difunieq  37362  pibt1  37404  wl-cbvmotv  37501  poimirlem25  37639  poimirlem30  37644  bndss  37780  fldcrngo  37998  flddmn  38052  xrnss3v  38354  trressn  38436  redundss3  38619  redundpim3  38621  eldisjim  38776  eldisjim2  38777  eldisjn0el  38798  partim  38800  mainer  38826  prter1  38872  sn-sup2  42479  rimcnv  42505  fimgmcyclem  42521  mzpclall  42715  setindtrs  43014  dgraalem  43134  oneptri  43246  ifpimim  43498  inintabss  43567  refimssco  43596  cotrintab  43603  intimass  43643  psshepw  43777  nzin  44307  axc11next  44395  iotaexeu  44407  hbexgVD  44895  orbitclmpt  44948  wfaxrep  44984  wfaxsep  44985  wfaxpow  44987  wfaxpr  44988  wfac8prim  44992  permaxinf2lem  45002  absnsb  47025  aovpcov0  47188  aov0ov0  47191  ichan  47453  ichal  47464  spr0el  47480  sprsymrelf  47493  enege  47643  onego  47644  gbogbow  47754  gpgvtxedg0  48051  gpgvtxedg1  48052  gpgprismgr4cycllem10  48091  sgrpplusgaopALT  48180  rhmsubcALTVlem3  48268  eluz2cnn0n1  48497  regt1loggt0  48522  rege1logbrege0  48544  rege1logbzge0  48545  relogbmulbexp  48547  islan2  49612