Theorem 3imtr4i 281

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  hbxfrbi  1792  nfntOLDOLD  1823  sbimi  1943  ralimi2  2978  reximi2  3039  r19.28v  3100  r19.29r  3102  r19.30  3111  elex  3243  rmoan  3439  rmoimi2  3442  sseq2  3660  rabss2  3718  n0rex  3968  undif4  4068  r19.2zb  4094  ralf0OLD  4112  difprsnss  4361  snsspw  4407  uniin  4489  iuniin  4563  iuneq1  4566  iuneq2  4569  iunpwss  4650  eunex  4889  rmorabex  4958  exss  4961  pwunss  5048  soeq2  5084  elopaelxp  5225  reliin  5273  coeq1  5312  coeq2  5313  cnveq  5328  dmeq  5356  dmin  5364  dmcoss  5417  rncoeq  5421  dminss  5582  imainss  5583  dfco2a  5673  iotaex  5906  fundif  5973  fununi  6002  fof  6153  f1ocnv  6187  foco2  6419  isocnv  6620  isotr  6626  oprabid  6717  resiexg  7144  zfrep6  7176  ovmptss  7303  dmtpos  7409  tposfn  7426  smores  7494  omopthlem1  7780  eqer  7822  ixpeq2  7964  enssdom  8022  fiprc  8080  sbthlem9  8119  infensuc  8179  fipwuni  8373  dfom3  8582  r1elss  8707  scott0  8787  fin56  9253  dominf  9305  ac6n  9345  brdom4  9390  dominfac  9433  inawina  9550  eltsk2g  9611  ltsosr  9953  ssxr  10145  recgt0ii  10967  sup2  11017  dfnn2  11071  peano2uz2  11503  eluzp1p1  11751  peano2uz  11779  zq  11832  ubmelfzo  12572  elfzlmr  12622  expclzlem  12924  wrdeq  13359  wwlktovf  13745  fsum2dlem  14545  fprod2dlem  14754  sin02gt0  14966  divalglem6  15168  qredeu  15419  isfunc  16571  xpcbas  16865  drsdirfi  16985  clatl  17163  tsrss  17270  gimcnv  17756  gsum2dlem1  18415  gsum2dlem2  18416  lmimcnv  19115  xrge0subm  19835  fctop  20856  cctop  20858  alexsubALTlem4  21901  lpbl  22355  xrge0gsumle  22683  xrge0tsms  22684  iirev  22775  iihalf1  22777  iihalf2  22779  iimulcl  22783  vitalilem1  23422  ply1idom  23929  aacjcl  24127  aannenlem2  24129  ang180lem4  24587  lgslem3  25069  axlowdim  25886  axcontlem2  25890  usgrexmplef  26196  cusgrop  26390  rusgrpropedg  26536  spthispth  26678  cycliscrct  26750  wwlksn0  26817  clwwlkn  26985  clwwlkccat  27332  clwwlknonccat  27334  numclwwlk1  27351  nmobndseqi  27762  axhcompl-zf  27983  hhcmpl  28185  shunssi  28355  spansni  28544  pjoml3i  28573  cmcmlem  28578  nonbooli  28638  lnopco0i  28991  pjnmopi  29135  pjnormssi  29155  hatomistici  29349  cvexchi  29356  cmdmdi  29404  mddmdin0i  29418  cdj3lem3b  29427  disjin  29525  disjin2  29526  xrge0tsmsd  29913  issgon  30314  sxbrsigalem0  30461  eulerpartlemgs2  30570  ballotlem2  30678  ballotth  30727  bnj945  30970  bnj556  31096  bnj557  31097  bnj607  31112  bnj864  31118  bnj969  31142  bnj999  31153  bnj1398  31228  elpotr  31810  dfon2lem8  31819  sltval2  31934  txpss3v  32110  meran1  32535  arg-ax  32540  bj-nfalt  32827  bj-eunex  32924  poimirlem25  33564  poimirlem30  33569  bndss  33715  fldcrng  33933  flddmn  33987  xrnss3v  34274  prter1  34483  mzpclall  37607  setindtrs  37909  dgraalem  38032  ifpimim  38171  inintabss  38201  refimssco  38230  cotrintab  38238  intimass  38263  psshepw  38399  nzin  38834  axc11next  38924  iotaexeu  38936  hbexgVD  39456  reuan  41501  aovpcov0  41591  aov0ov0  41594  enege  41883  onego  41884  gbogbow  41969  spr0el  42057  sprsymrelf  42070  mhmismgmhm  42131  sgrpplusgaopALT  42156  rhmisrnghm  42245  srhmsubclem1  42398  rhmsubcALTVlem3  42431  eluz2cnn0n1  42626  regt1loggt0  42655  rege1logbrege0  42677  rege1logbzge0  42678  relogbmulbexp  42680