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:  norassOLD  1535  hbxfrbi  1826  sbimiALT  2553  nexmo  2599  moimi  2603  eu6im  2635  ralimi2  3125  reximi2  3207  elisset  3452  elex  3459  rmoan  3678  rmoimi2  3682  reuan  3825  sseq2  3941  rabss2  4005  n0rex  4268  undif4  4374  r19.2zb  4399  difprsnss  4692  snsspw  4735  uniin  4824  iuniin  4893  iuneq1  4897  iuneq2  4900  iunpwss  4992  axrep6  5161  eunex  5256  rmorabex  5317  exss  5320  pwunssOLD  5420  soeq2  5459  elopaelxp  5605  reliin  5654  coeq1  5692  coeq2  5693  cnveq  5708  dmeq  5736  dmin  5744  dmcoss  5807  rncoeq  5811  dminss  5977  imainss  5978  dfco2a  6066  iotaex  6304  fundif  6373  fununi  6399  fof  6565  f1ocnv  6602  foco2  6850  isocnv  7062  isotr  7068  oprabidw  7166  oprabid  7167  zfrep6  7638  ovmptss  7771  dmtpos  7887  tposfn  7904  smores  7972  omopthlem1  8265  eqer  8307  ixpeq2  8458  enssdom  8517  fiprc  8578  sbthlem9  8619  infensuc  8679  fipwuni  8874  dfom3  9094  r1elss  9219  scott0  9299  fin56  9804  dominf  9856  ac6n  9896  brdom4  9941  dominfac  9984  inawina  10101  eltsk2g  10162  ltsosr  10505  ssxr  10699  recgt0ii  11535  sup2  11584  dfnn2  11638  peano2uz2  12058  eluzp1p1  12258  peano2uz  12289  ubmelfzo  13097  elfzlmr  13146  expclzlem  13449  wrdeq  13879  wwlktovf  14311  fsum2dlem  15117  fprod2dlem  15326  sin02gt0  15537  divalglem6  15739  qredeu  15992  isfunc  17126  xpcbas  17420  drsdirfi  17540  clatl  17718  tsrss  17825  smndex1mgm  18064  gimcnv  18399  gsum2dlem1  19083  gsum2dlem2  19084  lmimcnv  19832  xrge0subm  20132  fctop  21609  cctop  21611  alexsubALTlem4  22655  lpbl  23110  xrge0gsumle  23438  xrge0tsms  23439  iirev  23534  iihalf1  23536  iihalf2  23538  iimulcl  23542  vitalilem1  24212  ply1idom  24725  aacjcl  24923  aannenlem2  24925  ang180lem4  25398  lgslem3  25883  tgjustf  26267  axlowdim  26755  axcontlem2  26759  usgrexmplef  27049  cusgrop  27228  rusgrpropedg  27374  spthispth  27515  cycliscrct  27588  wwlksn0  27649  clwwlkccat  27775  clwwlkn  27811  clwwlknonccat  27881  numclwwlk1  28146  nmobndseqi  28562  axhcompl-zf  28781  hhcmpl  28983  shunssi  29151  spansni  29340  pjoml3i  29369  cmcmlem  29374  nonbooli  29434  lnopco0i  29787  pjnmopi  29931  pjnormssi  29951  hatomistici  30145  cvexchi  30152  cmdmdi  30200  mddmdin0i  30214  cdj3lem3b  30223  rmoun  30265  disjin  30349  disjin2  30350  xrge0tsmsd  30742  issgon  31492  sxbrsigalem0  31639  eulerpartlemgs2  31748  ballotlem2  31856  ballotth  31905  bnj945  32155  bnj556  32282  bnj557  32283  bnj607  32298  bnj864  32304  bnj969  32328  bnj999  32340  bnj1398  32416  elpotr  33139  dfon2lem8  33148  sltval2  33276  txpss3v  33452  meran1  33872  arg-ax  33877  bj-nfalt  34158  bj-imdirco  34605  difunieq  34791  pibt1  34833  wl-cbvmotv  34918  poimirlem25  35082  poimirlem30  35087  bndss  35224  fldcrng  35442  flddmn  35496  xrnss3v  35784  redundss3  36023  redundpim3  36025  prter1  36175  sn-sup2  39594  mzpclall  39668  setindtrs  39966  dgraalem  40089  ifpimim  40217  inintabss  40278  refimssco  40307  cotrintab  40314  intimass  40355  psshepw  40489  nzin  41022  axc11next  41110  iotaexeu  41122  hbexgVD  41612  absnsb  43619  aovpcov0  43746  aov0ov0  43749  ichan  43972  ichal  43983  spr0el  43999  sprsymrelf  44012  enege  44163  onego  44164  gbogbow  44274  mhmismgmhm  44426  sgrpplusgaopALT  44455  rhmisrnghm  44544  srhmsubclem1  44697  rhmsubcALTVlem3  44730  eluz2cnn0n1  44920  regt1loggt0  44950  rege1logbrege0  44972  rege1logbzge0  44973  relogbmulbexp  44975