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  1827  excomimw  2046  nexmo  2542  eu6im  2576  ralimi2  3070  reximi2  3071  rabid2im  3422  elexOLD  3452  rmoan  3686  rmoimi2  3690  reuan  3835  sstr2  3929  rabss2OLD  4019  n0rex  4298  undif4  4408  rzal  4435  difprsnss  4743  snsspw  4788  uniin  4875  iuniin  4947  iuneq1  4951  iuneq2  4954  iunpwss  5050  axrep6  5222  axrep6OLD  5223  eunex  5328  rmorabex  5408  exss  5411  soeq2  5555  reliin  5767  coeq1  5807  coeq2  5808  cnveq  5823  dmeq  5853  dmin  5861  dmcoss  5925  dmcossOLD  5926  rncoeq  5932  dminss  6112  imainss  6113  dfco2a  6205  fundif  6542  fununi  6568  fof  6747  f1ocnv  6787  foco2  7056  isocnv  7279  isotr  7285  oprabidw  7392  oprabid  7393  zfrep6OLD  7902  ovmptss  8037  dmtpos  8182  tposfn  8199  smores  8286  omopthlem1  8589  brinxper  8667  eqer  8674  fsetsspwxp  8794  ixpeq2  8853  enssdomOLD  8918  fiprc  8985  sbthlem9  9027  infensuc  9087  fipwuni  9333  dfom3  9562  ttrcltr  9631  r1elss  9724  scott0  9804  fin56  10309  dominf  10361  ac6n  10401  brdom4  10446  dominfac  10490  inawina  10607  eltsk2g  10668  ltsosr  11011  ssxr  11209  recgt0ii  12056  sup2  12106  dfnn2  12181  peano2uz2  12611  eluzp1p1  12810  peano2uz  12845  ubmelfzo  13679  elfzlmr  13731  expclzlem  14039  wrdeq  14492  wwlktovf  14912  fsum2dlem  15726  fprod2dlem  15939  sin02gt0  16153  divalglem6  16361  qredeu  16621  isfunc  17825  xpcbas  18138  drsdirfi  18265  clatl  18468  tsrss  18549  mhmismgmhm  18753  smndex1mgm  18872  gimcnv  19236  gsum2dlem1  19939  gsum2dlem2  19940  rhmisrnghm  20454  subrngrng  20521  srhmsubclem1  20648  fldidom  20742  lmimcnv  21057  xrge0subm  21436  fctop  22982  cctop  22984  alexsubALTlem4  24028  lpbl  24481  xrge0gsumle  24812  xrge0tsms  24813  iirev  24909  iihalf1  24911  iihalf2  24913  iimulcl  24917  vitalilem1  25588  ply1idom  26103  aacjcl  26307  aannenlem2  26309  ang180lem4  26792  lgslem3  27279  ltsval2  27637  madef  27845  lrrecfr  27952  norecdiv  28199  elons2  28267  dfn0s2  28341  nnaddscl  28355  nnmulscl  28356  znegscl  28401  uzsind  28414  zsoring  28418  z12negscl  28487  renegscl  28507  readdscl  28508  remulscl  28511  tgjustf  28558  axlowdim  29047  axcontlem2  29051  usgrexmplef  29345  cusgrop  29524  rusgrpropedg  29671  spthispth  29810  pthdifv  29816  cycliscrct  29885  wwlksn0  29949  clwwlkccat  30078  clwwlkn  30114  clwwlknonccat  30184  numclwwlk1  30449  nmobndseqi  30868  axhcompl-zf  31087  hhcmpl  31289  shunssi  31457  spansni  31646  pjoml3i  31675  cmcmlem  31680  nonbooli  31740  lnopco0i  32093  pjnmopi  32237  pjnormssi  32257  hatomistici  32451  cvexchi  32458  cmdmdi  32506  mddmdin0i  32520  cdj3lem3b  32529  rmoun  32581  disjin  32674  disjin2  32675  xrge0tsmsd  33152  issgon  34286  sxbrsigalem0  34434  eulerpartlemgs2  34543  ballotlem2  34652  ballotth  34701  bnj945  34935  bnj556  35061  bnj557  35062  bnj607  35077  bnj864  35083  bnj969  35107  bnj999  35119  bnj1398  35195  wevgblacfn  35310  elpotr  35980  dfon2lem8  35989  txpss3v  36077  meran1  36612  arg-ax  36617  bj-sbcex  36964  bj-nfalt  37029  bj-imdirco  37523  difunieq  37707  pibt1  37749  wl-cbvmotv  37855  poimirlem25  37983  poimirlem30  37988  bndss  38124  fldcrngo  38342  flddmn  38396  xrnss3v  38719  trressn  38873  redundss3  39050  redundpim3  39052  eldisjim  39225  eldisjim2  39226  eldisjn0el  39247  partim  39249  mainer  39286  prter1  39342  sn-sup2  42953  rimcnv  42979  fimgmcyclem  42995  mzpclall  43176  setindtrs  43474  dgraalem  43594  oneptri  43706  ifpimim  43957  inintabss  44026  refimssco  44055  cotrintab  44062  intimass  44102  psshepw  44236  nzin  44766  axc11next  44854  iotaexeu  44866  hbexgVD  45353  orbitclmpt  45406  wfaxrep  45442  wfaxsep  45443  wfaxpow  45445  wfaxpr  45446  wfac8prim  45450  permaxinf2lem  45460  absnsb  47490  aovpcov0  47653  aov0ov0  47656  muldvdsfacgt  47849  ichan  47930  ichal  47941  spr0el  47957  sprsymrelf  47970  enege  48136  onego  48137  gbogbow  48247  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgprismgr4cycllem10  48595  sgrpplusgaopALT  48686  rhmsubcALTVlem3  48774  eluz2cnn0n1  49002  regt1loggt0  49027  rege1logbrege0  49049  rege1logbzge0  49050  relogbmulbexp  49052  islan2  50116