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  2541  moimi  2545  eu6im  2575  ralimi2  3069  reximi2  3070  rabid2im  3453  elexOLD  3486  rmoan  3727  rmoimi2  3731  reuan  3876  sstr2  3970  rabss2  4058  n0rex  4337  undif4  4447  r19.2zb  4476  rzal  4489  difprsnss  4780  snsspw  4825  uniin  4912  iuniin  4985  iuneq1  4989  iuneq2  4992  iunpwss  5088  axrep6  5263  axrep6OLD  5264  eunex  5365  rmorabex  5440  exss  5443  soeq2  5588  elopaelxpOLD  5750  reliin  5801  coeq1  5842  coeq2  5843  cnveq  5858  dmeq  5888  dmin  5896  dmcoss  5959  rncoeq  5964  dminss  6147  imainss  6148  dfco2a  6240  iotaexOLD  6516  fundif  6590  fununi  6616  fof  6795  f1ocnv  6835  foco2  7104  isocnv  7328  isotr  7334  oprabidw  7441  oprabid  7442  zfrep6  7958  ovmptss  8097  dmtpos  8242  tposfn  8259  smores  8371  omopthlem1  8676  brinxper  8753  eqer  8760  fsetsspwxp  8872  ixpeq2  8930  enssdom  8996  fiprc  9064  sbthlem9  9110  infensuc  9174  fipwuni  9443  dfom3  9666  ttrcltr  9735  r1elss  9825  scott0  9905  fin56  10412  dominf  10464  ac6n  10504  brdom4  10549  dominfac  10592  inawina  10709  eltsk2g  10770  ltsosr  11113  ssxr  11309  recgt0ii  12153  sup2  12203  dfnn2  12258  peano2uz2  12686  eluzp1p1  12885  peano2uz  12922  ubmelfzo  13751  elfzlmr  13802  expclzlem  14106  wrdeq  14559  wwlktovf  14980  fsum2dlem  15791  fprod2dlem  16001  sin02gt0  16215  divalglem6  16422  qredeu  16682  isfunc  17882  xpcbas  18195  drsdirfi  18322  clatl  18523  tsrss  18604  mhmismgmhm  18774  smndex1mgm  18890  gimcnv  19255  gsum2dlem1  19956  gsum2dlem2  19957  rhmisrnghm  20445  subrngrng  20515  srhmsubclem1  20642  fldidom  20736  lmimcnv  21030  xrge0subm  21380  fctop  22947  cctop  22949  alexsubALTlem4  23993  lpbl  24447  xrge0gsumle  24778  xrge0tsms  24779  iirev  24879  iihalf1  24881  iihalf2  24884  iimulcl  24889  vitalilem1  25566  ply1idom  26087  aacjcl  26292  aannenlem2  26294  ang180lem4  26779  lgslem3  27267  sltval2  27625  madef  27821  lrrecfr  27907  norecdiv  28150  elons2  28216  dfn0s2  28281  nnaddscl  28295  nnmulscl  28296  znegscl  28337  uzsind  28350  zs12negscl  28397  renegscl  28406  readdscl  28407  remulscl  28410  tgjustf  28457  axlowdim  28945  axcontlem2  28949  usgrexmplef  29243  cusgrop  29422  rusgrpropedg  29569  spthispth  29711  pthdifv  29717  cycliscrct  29786  wwlksn0  29850  clwwlkccat  29976  clwwlkn  30012  clwwlknonccat  30082  numclwwlk1  30347  nmobndseqi  30765  axhcompl-zf  30984  hhcmpl  31186  shunssi  31354  spansni  31543  pjoml3i  31572  cmcmlem  31577  nonbooli  31637  lnopco0i  31990  pjnmopi  32134  pjnormssi  32154  hatomistici  32348  cvexchi  32355  cmdmdi  32403  mddmdin0i  32417  cdj3lem3b  32426  rmoun  32480  disjin  32572  disjin2  32573  xrge0tsmsd  33061  issgon  34159  sxbrsigalem0  34308  eulerpartlemgs2  34417  ballotlem2  34526  ballotth  34575  bnj945  34809  bnj556  34936  bnj557  34937  bnj607  34952  bnj864  34958  bnj969  34982  bnj999  34994  bnj1398  35070  wevgblacfn  35136  elpotr  35804  dfon2lem8  35813  txpss3v  35901  meran1  36434  arg-ax  36439  bj-nfalt  36734  bj-imdirco  37213  difunieq  37397  pibt1  37439  wl-cbvmotv  37536  poimirlem25  37674  poimirlem30  37679  bndss  37815  fldcrngo  38033  flddmn  38087  xrnss3v  38395  trressn  38468  redundss3  38651  redundpim3  38653  eldisjim  38807  eldisjim2  38808  eldisjn0el  38829  partim  38831  mainer  38857  prter1  38902  sn-sup2  42489  rimcnv  42515  fimgmcyclem  42531  mzpclall  42725  setindtrs  43024  dgraalem  43144  oneptri  43256  ifpimim  43508  inintabss  43577  refimssco  43606  cotrintab  43613  intimass  43653  psshepw  43787  nzin  44317  axc11next  44405  iotaexeu  44417  hbexgVD  44905  orbitclmpt  44958  wfaxrep  44994  wfaxsep  44995  wfaxpow  44997  wfaxpr  44998  wfac8prim  45002  permaxinf2lem  45012  absnsb  47036  aovpcov0  47199  aov0ov0  47202  ichan  47449  ichal  47460  spr0el  47476  sprsymrelf  47489  enege  47639  onego  47640  gbogbow  47750  gpgvtxedg0  48047  gpgvtxedg1  48048  gpgprismgr4cycllem10  48083  sgrpplusgaopALT  48150  rhmsubcALTVlem3  48238  eluz2cnn0n1  48467  regt1loggt0  48496  rege1logbrege0  48518  rege1logbzge0  48519  relogbmulbexp  48521  islan2  49481