Theorem 3imtr4i 294

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  norassOLD  1534  hbxfrbi  1825  sbimiOLD  2515  sbimiALT  2577  nexmo  2623  moimi  2627  eu6im  2660  ralimi2  3157  r19.28vOLD  3187  reximi2  3244  r19.29rOLD  3256  r19.30OLD  3339  elisset  3505  elex  3512  rmoan  3730  rmoimi2  3734  reuan  3880  sseq2  3993  rabss2  4054  n0rex  4314  undif4  4416  r19.2zb  4441  difprsnss  4732  snsspw  4775  uniin  4862  iuniin  4931  iuneq1  4935  iuneq2  4938  iunpwss  5029  axrep6  5197  eunex  5291  rmorabex  5352  exss  5355  pwunssOLD  5455  soeq2  5495  elopaelxp  5641  reliin  5690  coeq1  5728  coeq2  5729  cnveq  5744  dmeq  5772  dmin  5780  dmcoss  5842  rncoeq  5846  dminss  6010  imainss  6011  dfco2a  6099  iotaex  6335  fundif  6403  fununi  6429  fof  6590  f1ocnv  6627  foco2  6873  isocnv  7083  isotr  7089  oprabidw  7187  oprabid  7188  zfrep6  7656  ovmptss  7788  dmtpos  7904  tposfn  7921  smores  7989  omopthlem1  8282  eqer  8324  ixpeq2  8475  enssdom  8534  fiprc  8595  sbthlem9  8635  infensuc  8695  fipwuni  8890  dfom3  9110  r1elss  9235  scott0  9315  fin56  9815  dominf  9867  ac6n  9907  brdom4  9952  dominfac  9995  inawina  10112  eltsk2g  10173  ltsosr  10516  ssxr  10710  recgt0ii  11546  sup2  11597  dfnn2  11651  peano2uz2  12071  eluzp1p1  12271  peano2uz  12302  ubmelfzo  13103  elfzlmr  13152  expclzlem  13454  wrdeq  13886  wwlktovf  14320  fsum2dlem  15125  fprod2dlem  15334  sin02gt0  15545  divalglem6  15749  qredeu  16002  isfunc  17134  xpcbas  17428  drsdirfi  17548  clatl  17726  tsrss  17833  smndex1mgm  18072  gimcnv  18407  gsum2dlem1  19090  gsum2dlem2  19091  lmimcnv  19839  xrge0subm  20586  fctop  21612  cctop  21614  alexsubALTlem4  22658  lpbl  23113  xrge0gsumle  23441  xrge0tsms  23442  iirev  23533  iihalf1  23535  iihalf2  23537  iimulcl  23541  vitalilem1  24209  ply1idom  24718  aacjcl  24916  aannenlem2  24918  ang180lem4  25390  lgslem3  25875  tgjustf  26259  axlowdim  26747  axcontlem2  26751  usgrexmplef  27041  cusgrop  27220  rusgrpropedg  27366  spthispth  27507  cycliscrct  27580  wwlksn0  27641  clwwlkccat  27768  clwwlkn  27804  clwwlknonccat  27875  numclwwlk1  28140  nmobndseqi  28556  axhcompl-zf  28775  hhcmpl  28977  shunssi  29145  spansni  29334  pjoml3i  29363  cmcmlem  29368  nonbooli  29428  lnopco0i  29781  pjnmopi  29925  pjnormssi  29945  hatomistici  30139  cvexchi  30146  cmdmdi  30194  mddmdin0i  30208  cdj3lem3b  30217  rmoun  30258  disjin  30336  disjin2  30337  xrge0tsmsd  30692  issgon  31382  sxbrsigalem0  31529  eulerpartlemgs2  31638  ballotlem2  31746  ballotth  31795  bnj945  32045  bnj556  32172  bnj557  32173  bnj607  32188  bnj864  32194  bnj969  32218  bnj999  32230  bnj1398  32306  elpotr  33026  dfon2lem8  33035  sltval2  33163  txpss3v  33339  meran1  33759  arg-ax  33764  bj-nfalt  34045  difunieq  34658  pibt1  34700  wl-cbvmotv  34768  poimirlem25  34932  poimirlem30  34937  bndss  35079  fldcrng  35297  flddmn  35351  xrnss3v  35639  redundss3  35878  redundpim3  35880  prter1  36030  mzpclall  39373  setindtrs  39671  dgraalem  39794  ifpimim  39924  inintabss  39987  refimssco  40016  cotrintab  40023  intimass  40048  psshepw  40183  nzin  40699  axc11next  40787  iotaexeu  40799  hbexgVD  41289  absnsb  43311  aovpcov0  43438  aov0ov0  43441  ichal  43676  ichan  43679  spr0el  43693  sprsymrelf  43706  enege  43859  onego  43860  gbogbow  43970  mhmismgmhm  44122  sgrpplusgaopALT  44151  rhmisrnghm  44240  srhmsubclem1  44393  rhmsubcALTVlem3  44426  eluz2cnn0n1  44615  regt1loggt0  44645  rege1logbrege0  44667  rege1logbzge0  44668  relogbmulbexp  44670