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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  norassOLD  1536  hbxfrbi  1828  nexmo  2542  moimi  2546  eu6im  2576  ralimi2  3085  rexbiOLD  3175  reximi2  3176  elex  3451  rmoan  3675  rmoimi2  3679  reuan  3830  sseq2  3948  rabss2  4012  n0rex  4289  undif4  4401  r19.2zb  4427  rzal  4440  difprsnss  4733  snsspw  4776  uniin  4866  iuniin  4937  iuneq1  4941  iuneq2  4944  iunpwss  5037  axrep6  5217  eunex  5314  rmorabex  5376  exss  5379  pwunssOLD  5485  soeq2  5526  elopaelxpOLD  5678  reliin  5729  coeq1  5769  coeq2  5770  cnveq  5785  dmeq  5815  dmin  5823  dmcoss  5883  rncoeq  5887  dminss  6061  imainss  6062  dfco2a  6154  iotaex  6417  fundif  6490  fununi  6516  fof  6697  f1ocnv  6737  foco2  6992  isocnv  7210  isotr  7216  oprabidw  7315  oprabid  7316  zfrep6  7806  ovmptss  7942  dmtpos  8063  tposfn  8080  smores  8192  omopthlem1  8498  eqer  8542  fsetsspwxp  8650  ixpeq2  8708  enssdom  8774  fiprc  8844  sbthlem9  8887  infensuc  8951  fipwuni  9194  dfom3  9414  ttrcltr  9483  r1elss  9573  scott0  9653  fin56  10158  dominf  10210  ac6n  10250  brdom4  10295  dominfac  10338  inawina  10455  eltsk2g  10516  ltsosr  10859  ssxr  11053  recgt0ii  11890  sup2  11940  dfnn2  11995  peano2uz2  12417  eluzp1p1  12619  peano2uz  12650  ubmelfzo  13461  elfzlmr  13510  expclzlem  13815  wrdeq  14248  wwlktovf  14680  fsum2dlem  15491  fprod2dlem  15699  sin02gt0  15910  divalglem6  16116  qredeu  16372  isfunc  17588  xpcbas  17904  drsdirfi  18032  clatl  18235  tsrss  18316  smndex1mgm  18555  gimcnv  18892  gsum2dlem1  19580  gsum2dlem2  19581  lmimcnv  20338  fldidom  20585  xrge0subm  20648  fctop  22163  cctop  22165  alexsubALTlem4  23210  lpbl  23668  xrge0gsumle  24005  xrge0tsms  24006  iirev  24101  iihalf1  24103  iihalf2  24105  iimulcl  24109  vitalilem1  24781  ply1idom  25298  aacjcl  25496  aannenlem2  25498  ang180lem4  25971  lgslem3  26456  tgjustf  26843  axlowdim  27338  axcontlem2  27342  usgrexmplef  27635  cusgrop  27814  rusgrpropedg  27960  spthispth  28103  cycliscrct  28176  wwlksn0  28237  clwwlkccat  28363  clwwlkn  28399  clwwlknonccat  28469  numclwwlk1  28734  nmobndseqi  29150  axhcompl-zf  29369  hhcmpl  29571  shunssi  29739  spansni  29928  pjoml3i  29957  cmcmlem  29962  nonbooli  30022  lnopco0i  30375  pjnmopi  30519  pjnormssi  30539  hatomistici  30733  cvexchi  30740  cmdmdi  30788  mddmdin0i  30802  cdj3lem3b  30811  rmoun  30851  disjin  30934  disjin2  30935  xrge0tsmsd  31326  issgon  32100  sxbrsigalem0  32247  eulerpartlemgs2  32356  ballotlem2  32464  ballotth  32513  bnj945  32762  bnj556  32889  bnj557  32890  bnj607  32905  bnj864  32911  bnj969  32935  bnj999  32947  bnj1398  33023  elpotr  33766  dfon2lem8  33775  sltval2  33868  madef  34049  lrrecfr  34109  txpss3v  34189  meran1  34609  arg-ax  34614  bj-nfalt  34902  bj-imdirco  35370  difunieq  35554  pibt1  35596  wl-cbvmotv  35681  poimirlem25  35811  poimirlem30  35816  bndss  35953  fldcrng  36171  flddmn  36225  xrnss3v  36509  redundss3  36748  redundpim3  36750  prter1  36900  sn-sup2  40446  mzpclall  40556  setindtrs  40854  dgraalem  40977  ifpimim  41123  inintabss  41193  refimssco  41222  cotrintab  41229  intimass  41269  psshepw  41403  nzin  41943  axc11next  42031  iotaexeu  42043  hbexgVD  42533  absnsb  44532  aovpcov0  44693  aov0ov0  44696  ichan  44918  ichal  44929  spr0el  44945  sprsymrelf  44958  enege  45108  onego  45109  gbogbow  45219  mhmismgmhm  45371  sgrpplusgaopALT  45400  rhmisrnghm  45489  srhmsubclem1  45642  rhmsubcALTVlem3  45675  eluz2cnn0n1  45863  regt1loggt0  45893  rege1logbrege0  45915  rege1logbzge0  45916  relogbmulbexp  45918